let G be Group; :: thesis: for N being Subgroup of G
for a, b being Element of G st N is normal & b in N holds
for n being Nat ex g being Element of G st
( g in N & (a * b) |^ n = (a |^ n) * g )
let N be Subgroup of G; :: thesis: for a, b being Element of G st N is normal & b in N holds
for n being Nat ex g being Element of G st
( g in N & (a * b) |^ n = (a |^ n) * g )
let a, b be Element of G; :: thesis: ( N is normal & b in N implies for n being Nat ex g being Element of G st
( g in N & (a * b) |^ n = (a |^ n) * g ) )
assume A1: ( N is normal & b in N ) ; :: thesis: for n being Nat ex g being Element of G st
( g in N & (a * b) |^ n = (a |^ n) * g )
defpred S₁[ Nat] means for n being Nat ex g being Element of G st
( g in N & (a * b) |^ $1 = (a |^ $1) * g );
A2: (a * b) |^ 0 = 1_ G by GROUP_1:25;
(a |^ 0) * (1_ G) = (1_ G) * (1_ G) by GROUP_1:25
.= 1_ G by GROUP_1:def 4 ;
then A3: S₁[ 0 ] by A2, GROUP_2:46;

A4: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider g1 being Element of G such that
A5: ( g1 in N & (a * b) |^ n = (a |^ n) * g1 ) ;
A6: (a * b) |^ (n + 1) = ((a |^ n) * g1) * (a * b) by A5, GROUP_1:34
.= (a |^ n) * (g1 * (a * b)) by GROUP_1:def 3
.= (a |^ n) * ((g1 * a) * b) by GROUP_1:def 3 ;
a * N = N * a by A1, GROUP_3:117;
then g1 * a in a * N by A5, GROUP_2:104;
then consider g2 being Element of G such that
A7: ( g1 * a = a * g2 & g2 in N ) by GROUP_2:103;
(g1 * a) * b = a * (g2 * b) by A7, GROUP_1:def 3;
then (a |^ n) * ((g1 * a) * b) = ((a |^ n) * a) * (g2 * b) by GROUP_1:def 3
.= (a |^ (n + 1)) * (g2 * b) by GROUP_1:34 ;
hence S₁[n + 1] by A1, A6, A7, GROUP_2:50; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence for n being Nat ex g being Element of G st
( g in N & (a * b) |^ n = (a |^ n) * g ) ; :: thesis: verum