let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: - (0_. L) = 0_. L
set e = 0_. L;
set f = - (0_. L);
A1: for x being Nat st x < len (0_. L) holds
(0_. L) . x = (- (0_. L)) . x by POLYNOM4:3;
len (- (0_. L)) = len (0_. L) by POLYNOM4:8;
hence - (0_. L) = 0_. L by A1, ALGSEQ_1:12; :: thesis: verum