let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for k being Element of NAT holds
( (power L) . (- (1_ L)),(2 * k) = 1_ L & (power L) . (- (1_ L)),((2 * k) + 1) = - (1_ L) )
let k be Element of NAT ; :: thesis: ( (power L) . (- (1_ L)),(2 * k) = 1_ L & (power L) . (- (1_ L)),((2 * k) + 1) = - (1_ L) )
defpred S₁[ Nat] means ( (power L) . (- (1_ L)),(2 * $1) = 1_ L & (power L) . (- (1_ L)),((2 * $1) + 1) = - (1_ L) );

A1: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
A3: (power L) . (- (1_ L)),(2 * (k + 1)) = (power L) . (- (1_ L)),(((2 * k) + 1) + 1)
.= ((power L) . (- (1_ L)),((2 * k) + 1)) * (- (1_ L)) by GROUP_1:def 8
.= - ((1_ L) * (- (1_ L))) by A2, VECTSP_1:41
.= - (- (1_ L)) by VECTSP_1:def 19
.= 1_ L by RLVECT_1:30 ;
(power L) . (- (1_ L)),((2 * (k + 1)) + 1) = ((power L) . (- (1_ L)),(2 * (k + 1))) * (- (1_ L)) by GROUP_1:def 8
.= - (1_ L) by A3, VECTSP_1:def 19 ;
hence S₁[k + 1] by A3; :: thesis: verum

end;

(power L) . (- (1_ L)),((2 * 0 ) + 1) = ((power L) . (- (1_ L)),0 ) * (- (1_ L)) by GROUP_1:def 8
.= (1_ L) * (- (1_ L)) by GROUP_1:def 8
.= - (1_ L) by VECTSP_1:def 19 ;
then A4: S₁[ 0 ] by GROUP_1:def 8;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A1);
hence ( (power L) . (- (1_ L)),(2 * k) = 1_ L & (power L) . (- (1_ L)),((2 * k) + 1) = - (1_ L) ) ; :: thesis: verum