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

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

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (power L) . ((x * y),(n + 1)) = (((power L) . (x,n)) * ((power L) . (y,n))) * (x * y) by Def7
.= ((power L) . (x,n)) * (((power L) . (y,n)) * (x * y)) by Def3
.= ((power L) . (x,n)) * (x * (((power L) . (y,n)) * y)) by Def3
.= ((power L) . (x,n)) * (x * ((power L) . (y,(n + 1)))) by Def7
.= (((power L) . (x,n)) * x) * ((power L) . (y,(n + 1))) by Def3
.= ((power L) . (x,(n + 1))) * ((power L) . (y,(n + 1))) by Def7 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(power L) . ((x * y),0) = 1_ L by Def7
.= (1_ L) * (1_ L) by Def4
.= ((power L) . (x,0)) * (1_ L) by Def7
.= ((power L) . (x,0)) * ((power L) . (y,0)) by Def7 ;
then A2: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1); :: thesis: verum