I'm studying a proof of the product property of square roots. I can follow it up to statement 8, but I can't make sense of how the last statement, 9, follows from the previous ones. I have transcribed the proof below.
Product property of square roots: If $a$ and $b$ are real numbers such that $a \geq 0$ and $b \geq 0$, then $\sqrt{a} \cdot \sqrt{b} = \sqrt{ab}$.
$a \geq 0 \hbox{ and } b \geq 0.$
Given.
There is a unique non-negative number $\sqrt{a}$ such that $(\sqrt{a})^2 = a$. There is a unique non-negative number $\sqrt{b}$ such that $(\sqrt{b})^2 = b$.
Theorem 37.
$(\sqrt{a})^2(\sqrt{b})^2 = ab$
Multiplication property of equality.
$(\sqrt{a})^2(\sqrt{b})^2= (\sqrt{a} \cdot \sqrt{b})^2$
$a^nb^n = (a\cdot b)^n$
$(\sqrt{a} \cdot \sqrt{b})^2 = ab$
Transitive property of equality.
$\sqrt{a} \cdot \sqrt{b} \geq 0$
The product of non-negative numbers is non-negative.
$ab \geq 0$
The product of non-negative numbers is non-negative.
There is a unique non-negative number $\sqrt{ab}$ such that $(\sqrt{ab})^2 = ab$
Theorem 37.
$\sqrt{ab} = \sqrt{a}\sqrt{b}$
Theorem 37, steps 5, 6, and 8.
(Pearson, H. R and Allen, F. B. (1970). Modern Algebra - A Logical Approach (Book I). Boston: Ginn and Company, p. 508.)
Edit: I was asked to include Theorem 37, which is used in the proof. It is reproduced below.
Theorem 37:
If $a$ is a non-negative real number, then there is a unique non-negative real number denoted by $\sqrt{a}$ such that $(\sqrt{a})^2$.
I think a few steps are skipped from statement 8 to statement 9. I can see that
$$(\sqrt{ab})^2 = (\sqrt{a} \cdot \sqrt{b})^2$$
due to the transitive property of equality and statement 5, but I can't see how to go from there to 9 without assuming
$$(a^2 = b^2) \land (a \geq 0) \land (b \geq 0) \implies a = b. $$
And I can't figure out how to prove this last statement, although it seems to make intuitive sense. But maybe it's something else I'm missing.