let G be Group; :: thesis: for N being normal Subgroup of G
for a being Element of G
for S being Element of (G ./. N) st S = a * N holds
for n being Nat holds S |^ n = (a |^ n) * N
let N be normal Subgroup of G; :: thesis: for a being Element of G
for S being Element of (G ./. N) st S = a * N holds
for n being Nat holds S |^ n = (a |^ n) * N
let a be Element of G; :: thesis: for S being Element of (G ./. N) st S = a * N holds
for n being Nat holds S |^ n = (a |^ n) * N
let S be Element of (G ./. N); :: thesis: ( S = a * N implies for n being Nat holds S |^ n = (a |^ n) * N )
assume A1: S = a * N ; :: thesis: for n being Nat holds S |^ n = (a |^ n) * N
defpred S₁[ Nat] means for n being Nat holds S |^ $1 = (a |^ $1) * N;
A2: S |^ 0 = 1_ (G ./. N) by GROUP_1:25;
(a |^ 0) * N = (1_ G) * N by GROUP_1:25
.= carr N by GROUP_2:109 ;
then A3: S₁[ 0 ] by A2, GROUP_6:24;

A4: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
S |^ (n + 1) = (S |^ n) * S by GROUP_1:34
.= (@ (S |^ n)) * (@ S) by GROUP_6:def 3
.= ((a |^ n) * N) * (a * N) by A1, A5
.= ((a |^ n) * a) * N by GROUP_11:1
.= (a |^ (n + 1)) * N by GROUP_1:34 ;
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 S |^ n = (a |^ n) * N ; :: thesis: verum