let R be non empty unital associative commutative multMagma ; 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; for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)
let n be Nat; (a * b) |^ n = (a |^ n) * (b |^ n)
defpred S1[ Nat] means (power R) . ((a * b),$1) = (a |^ $1) * (b |^ $1);
A1:
now for m being Nat st S1[m] holds
S1[m + 1]let m be
Nat;
( S1[m] implies S1[m + 1] )reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
assume
S1[
m]
;
S1[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
S1[
m + 1]
;
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:
S1[ 0 ]
;
for m being Nat holds S1[m]
from NAT_1:sch 2(A2, A1);
hence
(a * b) |^ n = (a |^ n) * (b |^ n)
; verum