let L be non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 :: thesis: not - x = 0. L

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

end;

(- x) * (- (x ")) = - ((- x) * (x ")) by VECTSP_1:8
.= - (- (x * (x "))) by VECTSP_1:8
.= - (- (1_ L)) by A1, VECTSP_1:def 10
.= 1_ L by RLVECT_1:17 ;
hence - (x ") = (- x) " by A2, VECTSP_1:def 10; :: thesis: verum