now :: thesis:

let b1, b2 be non O -negative Element of R; :: thesis:
assume A: ( b1 ^2 = a & b2 ^2 = a ) ; :: thesis:
then A1: ( b1 is Sqrt of a & b2 is Sqrt of a ) by defsqrt;

per cases ;

suppose b1 = 0. R ; :: thesis:

hence b1 = b2 by A, VECTSP_2:def 1; :: thesis:

end;

suppose X: b1 <> 0. R ; :: thesis:

C: now :: thesis:

assume not 0. R <= O,b1 ; :: thesis:
then ( b1 <= O, 0. R & ( b1 < O, 0. R or b1 = 0. R ) ) by avb4;
hence contradiction by X, x2; :: thesis:

end;

now :: thesis:

assume not 0. R <= O,b2 ; :: thesis:
then ( b2 <= O, 0. R & ( b2 < O, 0. R or b2 = 0. R ) ) by avb4;
hence contradiction by x2, X, A, VECTSP_2:def 1; :: thesis:

end;

hence b1 = b2 by A1, C, sq0; :: thesis:

end;

end;

end;

hence for b₁, b₂ being non O -negative Sqrt of a st b₁ ^2 = a & b₂ ^2 = a holds
b₁ = b₂ ; :: thesis: