now :: thesis: for b1, b2 being non O -negative Element of R st b1 ^2 = a & b2 ^2 = a holds
b1 = b2

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

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

suppose b1 = 0. R ; :: thesis: b₁ = b₂

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

end;

suppose X: b1 <> 0. R ; :: thesis: b₁ = b₂

C: now :: thesis: 0. R <= O,b1

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

end;

now :: thesis: 0. R <= O,b2

assume not 0. R <= O,b2 ; :: thesis: contradiction
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: verum

end;

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

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: verum