for F being 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 ) )