let R be non empty unital associative commutative multMagma ; :: thesis: for a, b being Element of R
for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)
let a, b be Element of R; :: thesis: for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)
let n be Nat; :: thesis: (a * b) |^ n = (a |^ n) * (b |^ n)
defpred S₁[ Nat] means (power R) . ((a * b),$1) = (a |^ $1) * (b |^ $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] )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume S₁[m] ; :: thesis: S₁[m + 1]
then (power R) . ((a * b),(m + 1)) = (((power R) . (a,mm)) * ((power R) . (b,mm))) * (a * b) by GROUP_1:def 7
.= ((((power R) . (a,mm)) * ((power R) . (b,mm))) * a) * b by GROUP_1:def 3
.= ((((power R) . (a,mm)) * a) * ((power R) . (b,mm))) * b by GROUP_1:def 3
.= (((power R) . (a,mm)) * a) * (((power R) . (b,mm)) * b) by GROUP_1:def 3
.= (a |^ (m + 1)) * (((power R) . (b,mm)) * b) by GROUP_1:def 7
.= (a |^ (m + 1)) * (b |^ (m + 1)) by GROUP_1:def 7 ;
hence S₁[m + 1] ; :: thesis: verum

end;

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