let R be non empty unital associative commutative multMagma ; :: thesis: for a, b being Element of R
for n being Element of NAT holds (a * b) |^ n = (a |^ n) * (b |^ n)
let a, b be Element of R; :: thesis: for n being Element of NAT holds (a * b) |^ n = (a |^ n) * (b |^ n)
let n be Element of NAT ; :: thesis: (a * b) |^ n = (a |^ n) * (b |^ n)
defpred S₁[ Element of NAT ] means (power R) . ((a * b),$1) = ((power R) . (a,$1)) * ((power R) . (b,$1));

A1: now

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 8
.= ((((power R) . (a,m)) * ((power R) . (b,m))) * a) * b by GROUP_1:def 4
.= ((((power R) . (a,m)) * a) * ((power R) . (b,m))) * b by GROUP_1:def 4
.= (((power R) . (a,m)) * a) * (((power R) . (b,m)) * b) by GROUP_1:def 4
.= ((power R) . (a,(m + 1))) * (((power R) . (b,m)) * b) by GROUP_1:def 8
.= ((power R) . (a,(m + 1))) * ((power R) . (b,(m + 1))) by GROUP_1:def 8 ;
hence S₁[m + 1] ; :: thesis: verum

end;

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