let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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

A2: now

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

end;

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: (power L) . ((- (1_ L)),(k + 1)) = ((power L) . ((- (1_ L)),k)) * (- (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 Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A1);
hence (power L) . ((- (1_ L)),k) <> 0. L ; :: thesis: verum