let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N' being normal Subgroup of G st N' = multMagma(# the carrier of N,the multF of N #) holds
( G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) & 1_ (G ./. N') = 1_ (G ./. N) )
let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G
for N' being normal Subgroup of G st N' = multMagma(# the carrier of N,the multF of N #) holds
( G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) & 1_ (G ./. N') = 1_ (G ./. N) )
let N be normal StableSubgroup of G; :: thesis: for N' being normal Subgroup of G st N' = multMagma(# the carrier of N,the multF of N #) holds
( G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) & 1_ (G ./. N') = 1_ (G ./. N) )
let N' be normal Subgroup of G; :: thesis: ( N' = multMagma(# the carrier of N,the multF of N #) implies ( G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) & 1_ (G ./. N') = 1_ (G ./. N) ) )
assume A1: N' = multMagma(# the carrier of N,the multF of N #) ; :: thesis: ( G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) & 1_ (G ./. N') = 1_ (G ./. N) )
then Cosets N' = Cosets N by Def14;
hence G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) by A1, Def15; :: thesis: 1_ (G ./. N') = 1_ (G ./. N)
reconsider e = 1_ (G ./. N') as Element of (G ./. N) by A1, Def14;

now

let h be Element of (G ./. N); :: thesis: ( h * e = h & e * h = h )
reconsider h' = h as Element of (G ./. N') by A1, Def14;
thus h * e = h' * (1_ (G ./. N')) by A1, Def15
.= h by GROUP_1:def 5 ; :: thesis: e * h = h
thus e * h = (1_ (G ./. N')) * h' by A1, Def15
.= h by GROUP_1:def 5 ; :: thesis: verum

end;

hence 1_ (G ./. N') = 1_ (G ./. N) by GROUP_1:10; :: thesis: verum