let L be non empty associative well-unital 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) );
1_ L = 1. L ;
then ((power L) . x,k1) * ((power L) . x,0 ) = ((power L) . x,k1) * (1. L) by GROUP_1:def 8
.= (power L) . x,(k1 + 0 ) by VECTSP_1:def 13 ;
then A1: S₁[ 0 ] ;

A2: now

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A3: S₁[j] ; :: thesis: S₁[j + 1]
((power L) . x,k1) * ((power L) . x,(j + 1)) = ((power L) . x,k1) * (((power L) . x,j) * x) by GROUP_1:def 8
.= (((power L) . x,k1) * ((power L) . x,j)) * x by GROUP_1:def 4
.= (power L) . x,((k1 + j) + 1) by A3, GROUP_1:def 8
.= (power L) . x,(k1 + (j + 1)) ;
hence S₁[j + 1] ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
then consider j being Element of NAT such that
A4: ( j = k2 & ((power L) . x,k1) * ((power L) . x,j) = (power L) . x,(k1 + j) ) ;
thus ((power L) . x,k1) * ((power L) . x,k2) = (power L) . x,(k1 + k2) by A4; :: thesis: verum