theorem Th1: :: EC_PF_2:1

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