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₁[ Element of NAT ] means (power L) . a,(n + $1) = ((power L) . a,n) * ((power L) . a,$1);
(power L) . a,(n + 0 ) = ((power L) . a,n) * (1_ L) by GROUP_1:def 5
.= ((power L) . a,n) * ((power L) . a,0 ) by GROUP_1:def 8 ;
then A1: S₁[ 0 ] ;

A2: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: 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 A3, GROUP_1:def 8
.= ((power L) . a,n) * (((power L) . a,m) * a) by GROUP_1:def 4
.= ((power L) . a,n) * ((power L) . a,(m + 1)) by GROUP_1:def 8 ;
hence S₁[m + 1] ; :: thesis: verum

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A1, A2);
hence (power L) . a,(n + m) = ((power L) . a,n) * ((power L) . a,m) ; :: thesis: verum