let F be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for x, y being Element of F holds
( x * x = y * y iff ( x = y or x = - y ) )
let x, y be Element of F; :: thesis: ( x * x = y * y iff ( x = y or x = - y ) )
A1: (x - y) * (x + y) = ((x - y) * x) + ((x - y) * y) by VECTSP_1:def 7
.= ((x * x) - (x * y)) + ((x - y) * y) by VECTSP_1:11
.= ((x * x) - (x * y)) + ((y * x) - (y * y)) by VECTSP_1:11
.= (((x * x) - (x * y)) + (y * x)) + (- (y * y)) by RLVECT_1:def 3
.= ((x * x) + ((- (x * y)) + (y * x))) + (- (y * y)) by RLVECT_1:def 3
.= ((x * x) + ((y * x) - (x * y))) + (- (y * y))
.= ((x * x) + ((x - x) * y)) + (- (y * y)) by VECTSP_1:11
.= ((x * x) + ((0. F) * y)) - (y * y) by RLVECT_1:5
.= ((x * x) + (0. F)) - (y * y)
.= (x * x) - (y * y) by RLVECT_1:def 4 ;

hereby :: thesis: ( ( x = y or x = - y ) implies x * x = y * y )

assume A2: x * x = y * y ; :: thesis: ( x = y or x = - y )
(x - y) * (x + y) = 0. F by A1, A2, RLVECT_1:5;
then ( x - y = 0. F or x + y = 0. F ) by VECTSP_1:12;
hence ( x = y or x = - y ) by RLVECT_1:6, RLVECT_1:21; :: thesis: verum

end;

assume ( x = y or x = - y ) ; :: thesis: x * x = y * y
then ( x - y = 0. F or x + y = 0. F ) by RLVECT_1:5;
hence x * x = y * y by A1, RLVECT_1:21; :: thesis: verum