let R be ordered domRing; :: thesis: for O being Ordering of R
for a being square Element of R
for b being Element of R holds
( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )
let O be Ordering of R; :: thesis: for a being square Element of R
for b being Element of R holds
( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )
let a be square Element of R; :: thesis: for b being Element of R holds
( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )
let b be Element of R; :: thesis: ( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )

hereby :: thesis: ( ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) implies b is Sqrt of a )

assume b is Sqrt of a ; :: thesis: ( b = sqrt (O,a) or b = - (sqrt (O,a)) )
then b ^2 = a by defsqrt
.= (sqrt (O,a)) ^2 by defq ;
hence ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) by sq00; :: thesis: verum

end;

assume ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) ; :: thesis: b is Sqrt of a

per cases then ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) ;

suppose b = sqrt (O,a) ; :: thesis: b is Sqrt of a

hence b is Sqrt of a ; :: thesis: verum

end;

suppose B: b = - (sqrt (O,a)) ; :: thesis: b is Sqrt of a

(- (sqrt (O,a))) ^2 = (sqrt (O,a)) ^2 by VECTSP_1:10;
hence b is Sqrt of a by B, defsqrt; :: thesis: verum

end;

end;