definition of sqrt(x)

[triclino]

Can the following two definitions of sqrt(x) be considered as equivalent??

 

 

1) if [math]x\geq 0[/math] ,then ([math]\sqrt x=y[/math]) if ([math]y^2=x\wedge y\geq 0[/math])

 

 

2) if [math]x\geq 0[/math] ,then ([math]\sqrt x=y[/math]) iff ([math]y^2=x\wedge y\geq 0[/math])

[the tree]

Since the positive square root function is single valued and monotonic, I would say so.

[triclino]

If they are equivalent we must have:

 

(1) implying (2) and (2) implying (1) .

 

I can see that (2) implies (1) ,but how does (1) imply (2)??