let L be non empty unital associative multMagma ; :: thesis: for x being Element of L
for n, m being 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 Nat holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m)
let n be Nat; :: thesis: for m being Nat holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m)
defpred S₁[ Nat] means (power L) . (x,(n * $1)) = (power L) . (((power L) . (x,n)),$1);
set pL = power L;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
reconsider nm = n * m, mm = m as Element of NAT by ORDINAL1:def 12;
(power L) . (x,(n * (m + 1))) = (power L) . (x,((n * m) + (n * 1)))
.= ((power L) . (x,nm)) * ((power L) . (x,nn)) by POLYNOM2:1
.= (power L) . (((power L) . (x,nn)),(mm + 1)) by A2, GROUP_1:def 7 ;
hence S₁[m + 1] ; :: thesis: verum

end;

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