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)
A1: n in NAT by ORDINAL1:def 12;
defpred S₁[ Element of NAT ] means (power R) . ((a * b),$1) = ((power R) . (a,$1)) * ((power R) . (b,$1));

A2: now :: thesis: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then (power R) . ((a * b),(m + 1)) = (((power R) . (a,m)) * ((power R) . (b,m))) * (a * b) by GROUP_1:def 7
.= ((((power R) . (a,m)) * ((power R) . (b,m))) * a) * b by GROUP_1:def 3
.= ((((power R) . (a,m)) * a) * ((power R) . (b,m))) * b by GROUP_1:def 3
.= (((power R) . (a,m)) * a) * (((power R) . (b,m)) * b) by GROUP_1:def 3
.= ((power R) . (a,(m + 1))) * (((power R) . (b,m)) * b) by GROUP_1:def 7
.= ((power R) . (a,(m + 1))) * ((power R) . (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 A3: S₁[ 0 ] ;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A3, A2);
hence (a * b) |^ n = (a |^ n) * (b |^ n) by A1; :: thesis: verum