let R be preordered domRing; :: thesis: for P being Preordering of R
for a being square Element of R
for b1, b2 being Sqrt of a st 0. R <= P,b1 & 0. R <= P,b2 holds
b1 = b2
let P be Preordering of R; :: thesis: for a being square Element of R
for b1, b2 being Sqrt of a st 0. R <= P,b1 & 0. R <= P,b2 holds
b1 = b2
let a be square Element of R; :: thesis: for b1, b2 being Sqrt of a st 0. R <= P,b1 & 0. R <= P,b2 holds
b1 = b2
let b1, b2 be Sqrt of a; :: thesis: ( 0. R <= P,b1 & 0. R <= P,b2 implies b1 = b2 )
assume AS: ( 0. R <= P,b1 & 0. R <= P,b2 ) ; :: thesis: b1 = b2

per cases ( b1 = 0. R or b1 <> 0. R ) ;

suppose A: b1 = 0. R ; :: thesis: b1 = b2

then 0. R = b1 ^2
.= a by defsqrt
.= b2 ^2 by defsqrt
.= b2 * b2 ;
hence b1 = b2 by A, VECTSP_2:def 1; :: thesis: verum

end;

suppose b1 <> 0. R ; :: thesis: b1 = b2

then A: - b1 < P, - (0. R) by AS, c10a;
b1 ^2 = a by defsqrt
.= b2 ^2 by defsqrt ;
then ( b1 = b2 or b1 = - b2 ) by sq00;
hence b1 = b2 by A, AS, c2; :: thesis: verum

end;

end;