let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for x being Element of L st x <> 0. L holds
- (x " ) = (- x) "
let x be Element of L; :: thesis: ( x <> 0. L implies - (x " ) = (- x) " )
assume A1: x <> 0. L ; :: thesis: - (x " ) = (- x) "

A2: now

assume - x = 0. L ; :: thesis: contradiction
then - (- x) = 0. L by RLVECT_1:25;
hence contradiction by A1, RLVECT_1:30; :: thesis: verum

end;

(- x) * (- (x " )) = - ((- x) * (x " )) by VECTSP_1:40
.= - (- (x * (x " ))) by VECTSP_1:40
.= - (- (1_ L)) by A1, VECTSP_1:def 22
.= 1_ L by RLVECT_1:30 ;
hence - (x " ) = (- x) " by A2, VECTSP_1:def 22; :: thesis: verum