let R be domRing; :: thesis: for a, b being Element of R holds
( a ^2 = b ^2 iff ( a = b or a = - b ) )
let a, b be Element of R; :: thesis: ( a ^2 = b ^2 iff ( a = b or a = - b ) )

hereby :: thesis: ( ( a = b or a = - b ) implies a ^2 = b ^2 )

assume a ^2 = b ^2 ; :: thesis: ( a = b or a = - b )
then 0. R = (a ^2) - (b ^2) by RLVECT_1:15
.= (a + b) * (a - b) by P4a ;

per cases then ( a + b = 0. R or a - b = 0. R ) by VECTSP_2:def 1;

suppose a + b = 0. R ; :: thesis: ( a = b or a = - b )

hence ( a = b or a = - b ) by RLVECT_1:6; :: thesis: verum

end;

suppose a - b = 0. R ; :: thesis: ( a = b or a = - b )

hence ( a = b or a = - b ) by RLVECT_1:21; :: thesis: verum

end;

end;

end;

assume ( a = b or a = - b ) ; :: thesis: a ^2 = b ^2

per cases then ( a = b or a = - b ) ;

suppose a = b ; :: thesis: a ^2 = b ^2

hence a ^2 = b ^2 ; :: thesis: verum

end;

suppose a = - b ; :: thesis: a ^2 = b ^2

hence a ^2 = b ^2 by VECTSP_1:10; :: thesis: verum

end;

end;