let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for k being Element of NAT holds (power L) . ((- (1_ L)),k) <> 0. L
let k be Element of NAT ; :: thesis: (power L) . ((- (1_ L)),k) <> 0. L
defpred S₁[ Nat] means (power L) . ((- (1_ L)),$1) <> 0. L;

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

A2: now :: thesis: not - (1_ L) = 0. L

assume A3: - (1_ L) = 0. L ; :: thesis: contradiction
1_ L = (1_ L) * (1_ L)
.= (- (1_ L)) * (- (1_ L)) by VECTSP_1:10
.= 0. L by A3 ;
hence contradiction ; :: thesis: verum

end;

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
A4: (power L) . ((- (1_ L)),(kk + 1)) = ((power L) . ((- (1_ L)),kk)) * (- (1_ L)) by GROUP_1:def 7;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A4, A2, VECTSP_1:12; :: thesis: verum

end;

A5: S₁[ 0 ] by GROUP_1:def 7;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A1);
hence (power L) . ((- (1_ L)),k) <> 0. L ; :: thesis: verum