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 S1[ Nat] means ( (power L) . ((- (1_ L)),(2 * $1)) = 1_ L & (power L) . ((- (1_ L)),((2 * $1) + 1)) = - (1_ L) );
A1: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[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 7
.= - ((1_ L) * (- (1_ L))) by A2, VECTSP_1:9
.= - (- (1_ L))
.= 1_ L by RLVECT_1:17 ;
(power L) . ((- (1_ L)),((2 * (k + 1)) + 1)) = ((power L) . ((- (1_ L)),(2 * (k + 1)))) * (- (1_ L)) by GROUP_1:def 7
.= - (1_ L) by A3 ;
hence S1[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 7
.= (1_ L) * (- (1_ L)) by GROUP_1:def 7
.= - (1_ L) ;
then A4: S1[ 0 ] by GROUP_1:def 7;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A1);
 hence ( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) ) ; :: thesis: verum