for F being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr
for a being Element of F holds a |^ 2 = (- a) |^ 2