let p be Prime; :: thesis: for G being finite Group
for a, b being Element of G st G is p -commutative-group-like holds
for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n))
let G be finite Group; :: thesis: for a, b being Element of G st G is p -commutative-group-like holds
for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n))
let a, b be Element of G; :: thesis: ( G is p -commutative-group-like implies for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) )
assume A1: G is p -commutative-group-like ; :: thesis: for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n))
defpred S₁[ Nat] means for n being Nat holds (a * b) |^ (p |^ $1) = (a |^ (p |^ $1)) * (b |^ (p |^ $1));
A2: (a * b) |^ (p |^ 0) = (a * b) |^ 1 by NEWTON:4
.= a * b by GROUP_1:26 ;
(a |^ (p |^ 0)) * (b |^ (p |^ 0)) = (a |^ 1) * (b |^ (p |^ 0)) by NEWTON:4
.= a * (b |^ (p |^ 0)) by GROUP_1:26
.= a * (b |^ 1) by NEWTON:4
.= a * b by GROUP_1:26 ;
then A3: S₁[ 0 ] by A2;

A4: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
set a1 = a |^ (p |^ n);
set b1 = b |^ (p |^ n);
(a * b) |^ (p |^ (n + 1)) = (a * b) |^ ((p |^ n) * p) by NEWTON:6
.= ((a * b) |^ (p |^ n)) |^ p by GROUP_1:35
.= ((a |^ (p |^ n)) * (b |^ (p |^ n))) |^ p by A5
.= ((a |^ (p |^ n)) |^ p) * ((b |^ (p |^ n)) |^ p) by A1
.= (a |^ ((p |^ n) * p)) * ((b |^ (p |^ n)) |^ p) by GROUP_1:35
.= (a |^ ((p |^ n) * p)) * (b |^ ((p |^ n) * p)) by GROUP_1:35
.= (a |^ (p |^ (n + 1))) * (b |^ ((p |^ n) * p)) by NEWTON:6
.= (a |^ (p |^ (n + 1))) * (b |^ (p |^ (n + 1))) by NEWTON:6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) ; :: thesis: verum