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

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

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
(power L) . (a,(n + (m + 1))) = (power L) . (a,((n + m) + 1))
.= (((power L) . (a,n)) * ((power L) . (a,m))) * a by A2, GROUP_1:def 7
.= ((power L) . (a,n)) * (((power L) . (a,m)) * a) by GROUP_1:def 3
.= ((power L) . (a,n)) * ((power L) . (a,(m + 1))) by GROUP_1:def 7 ;
hence S₁[m + 1] ; :: thesis: verum

end;

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