let F be non empty right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; 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; ( 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 ( ( x = y or x = - y ) implies x * x = y * y )
end;
assume
( x = y or x = - y )
; 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; verum