theorem :: ALGSTR_2:8

for G being Abelian left-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G