for G, F being non empty right_complementable add-associative right_zeroed addLoopStr
for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]