let O be set ; :: thesis: for G being strict GroupWithOperators of O
for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of G = (nat_hom N) " the carrier of H holds
H = (Omega). (G ./. N)
let G be strict GroupWithOperators of O; :: thesis: for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of G = (nat_hom N) " the carrier of H holds
H = (Omega). (G ./. N)
let N be strict normal StableSubgroup of G; :: thesis: for H being strict StableSubgroup of G ./. N st the carrier of G = (nat_hom N) " the carrier of H holds
H = (Omega). (G ./. N)
let H be strict StableSubgroup of G ./. N; :: thesis: ( the carrier of G = (nat_hom N) " the carrier of H implies H = (Omega). (G ./. N) )
reconsider N' = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
reconsider H' = multMagma(# the carrier of H,the multF of H #) as strict Subgroup of G ./. N by Lm16;
A1: ( the carrier of H' c= the carrier of (G ./. N) & the multF of H' = the multF of (G ./. N) || the carrier of H' ) by GROUP_2:def 5;
A2: the carrier of (G ./. N) = the carrier of (G ./. N') by Def14;
the multF of (G ./. N) = the multF of (G ./. N') by Def15;
then reconsider H' = H' as strict Subgroup of G ./. N' by A1, A2, GROUP_2:def 5;
assume the carrier of G = (nat_hom N) " the carrier of H ; :: thesis: H = (Omega). (G ./. N)
then A3: the carrier of G = (nat_hom N') " the carrier of H' by Def23;

now

let h be Element of (G ./. N'); :: thesis: ( ( h in H' implies h in (Omega). (G ./. N') ) & ( h in (Omega). (G ./. N') implies h in H' ) )
thus ( h in H' implies h in (Omega). (G ./. N') ) by STRUCT_0:def 5; :: thesis: ( h in (Omega). (G ./. N') implies h in H' )
assume h in (Omega). (G ./. N') ; :: thesis: h in H'
h in Left_Cosets N' ;
then consider g being Element of G such that
A4: h = g * N' by GROUP_2:def 15;
reconsider R = nat_hom N' as Relation of the carrier of G,the carrier of (G ./. N') ;
consider h' being Element of (G ./. N') such that
A5: ( [g,h'] in R & h' in the carrier of H' ) by A3, RELSET_1:53;
(nat_hom N') . g = h' by A5, FUNCT_1:8;
then h in the carrier of H' by A4, A5, GROUP_6:def 9;
hence h in H' by STRUCT_0:def 5; :: thesis: verum

end;

then H' = (Omega). (G ./. N') by GROUP_2:def 6;
then the carrier of H = Cosets N by Def14;
hence H = (Omega). (G ./. N) by Lm5; :: thesis: verum