let L be non empty unital associative multMagma ; :: thesis: for x being Element of L
for n, m being Element of NAT holds (power L) . x,(n * m) = (power L) . ((power L) . x,n),m
let x be Element of L; :: thesis: for n, m being Element of NAT holds (power L) . x,(n * m) = (power L) . ((power L) . x,n),m
let n be Element of NAT ; :: thesis: for m being Element of NAT holds (power L) . x,(n * m) = (power L) . ((power L) . x,n),m
defpred S₁[ Element of NAT ] means (power L) . x,(n * $1) = (power L) . ((power L) . x,n),$1;
set pL = power L;
A1: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
thus (power L) . x,(n * (m + 1)) = (power L) . x,((n * m) + (n * 1))
.= ((power L) . x,(n * m)) * ((power L) . x,n) by POLYNOM2:2
.= (power L) . ((power L) . x,n),(m + 1) by A2, GROUP_1:def 8 ; :: thesis: verum

end;

(power L) . x,(n * 0 ) = 1_ L by GROUP_1:def 8
.= (power L) . ((power L) . x,n),0 by GROUP_1:def 8 ;
then A3: S₁[ 0 ] ;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A3, A1); :: thesis: verum