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