let L be non empty unital associative multMagma ; :: thesis: for x being Element of L
for n, m being Nat holds () . (x,(n * m)) = () . ((() . (x,n)),m)

let x be Element of L; :: thesis: for n, m being Nat holds () . (x,(n * m)) = () . ((() . (x,n)),m)
let n be Nat; :: thesis: for m being Nat holds () . (x,(n * m)) = () . ((() . (x,n)),m)
defpred S1[ Nat] means () . (x,(n * \$1)) = () . ((() . (x,n)),\$1);
set pL = power L;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; :: thesis: S1[m + 1]
reconsider nm = n * m, mm = m as Element of NAT by ORDINAL1:def 12;
() . (x,(n * (m + 1))) = () . (x,((n * m) + (n * 1)))
.= (() . (x,nm)) * (() . (x,nn)) by POLYNOM2:1
.= () . ((() . (x,nn)),(mm + 1)) by ;
hence S1[m + 1] ; :: thesis: verum
end;
() . (x,(n * 0)) = 1_ L by GROUP_1:def 7
.= () . ((() . (x,nn)),0) by GROUP_1:def 7 ;
then A3: S1[ 0 ] ;
thus for m being Nat holds S1[m] from NAT_1:sch 2(A3, A1); :: thesis: verum