let L be non empty unital associative commutative multMagma ; :: thesis: for x, y being Element of L
for n being Element of 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 Element of NAT holds (power L) . (x * y),n = ((power L) . x,n) * ((power L) . y,n)
defpred S₁[ Element of NAT ] means (power L) . (x * y),$1 = ((power L) . x,$1) * ((power L) . y,$1);

A1: now

let n be Element of 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 Def8
.= ((power L) . x,n) * (((power L) . y,n) * (x * y)) by Def4
.= ((power L) . x,n) * (x * (((power L) . y,n) * y)) by Def4
.= ((power L) . x,n) * (x * ((power L) . y,(n + 1))) by Def8
.= (((power L) . x,n) * x) * ((power L) . y,(n + 1)) by Def4
.= ((power L) . x,(n + 1)) * ((power L) . y,(n + 1)) by Def8 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(power L) . (x * y),0 = 1_ L by Def8
.= (1_ L) * (1_ L) by Def5
.= ((power L) . x,0 ) * (1_ L) by Def8
.= ((power L) . x,0 ) * ((power L) . y,0 ) by Def8 ;
then A2: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1); :: thesis: verum