let L be non empty well-unital associative multLoopStr ; :: thesis: for x being Element of L
for k1, k2 being Element of NAT holds ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))
let x be Element of L; :: thesis: for k1, k2 being Element of NAT holds ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))
let k1, k2 be Element of NAT ; :: thesis: ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))
defpred S₁[ Nat] means ex j being Element of NAT st
( j = $1 & ((power L) . (x,k1)) * ((power L) . (x,j)) = (power L) . (x,(k1 + j)) );

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

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
assume A2: S₁[j] ; :: thesis: S₁[j + 1]
((power L) . (x,k1)) * ((power L) . (x,(j + 1))) = ((power L) . (x,k1)) * (((power L) . (x,jj)) * x) by GROUP_1:def 7
.= (((power L) . (x,k1)) * ((power L) . (x,jj))) * x by GROUP_1:def 3
.= (power L) . (x,((k1 + j) + 1)) by A2, GROUP_1:def 7
.= (power L) . (x,(k1 + (j + 1))) ;
hence S₁[j + 1] ; :: thesis: verum

end;

1_ L = 1. L ;
then ((power L) . (x,k1)) * ((power L) . (x,0)) = ((power L) . (x,k1)) * (1. L) by GROUP_1:def 7
.= (power L) . (x,(k1 + 0)) ;
then A3: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
then ex j being Element of NAT st
( j = k2 & ((power L) . (x,k1)) * ((power L) . (x,j)) = (power L) . (x,(k1 + j)) ) ;
hence ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2)) ; :: thesis: verum