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: S₁[ 0 ] by GROUP_1:def 8;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: (power L) . (- (1_ L)),(k + 1) = ((power L) . (- (1_ L)),k) * (- (1_ L)) by GROUP_1:def 8;

now

assume A5: - (1_ L) = 0. L ; :: thesis: contradiction
1_ L = (1_ L) * (1_ L) by VECTSP_1:def 13
.= (- (1_ L)) * (- (1_ L)) by VECTSP_1:42
.= 0. L by A5, VECTSP_1:36 ;
hence contradiction ; :: thesis: verum

end;

hence S₁[k + 1] by A3, A4, VECTSP_1:44; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence (power L) . (- (1_ L)),k <> 0. L ; :: thesis: verum