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)
reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
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 H9 = multMagma(# the carrier of H, the multF of H #) as strict Subgroup of G ./. N by Lm15;
A1: ( the carrier of H9 c= the carrier of (G ./. N) & the multF of H9 = the multF of (G ./. N) || the carrier of H9 ) by GROUP_2:def 5;
( the carrier of (G ./. N) = the carrier of (G ./. N9) & the multF of (G ./. N) = the multF of (G ./. N9) ) by Def14, Def15;
then reconsider H9 = H9 as strict Subgroup of G ./. N9 by A1, GROUP_2:def 5;
assume the carrier of G = (nat_hom N) " the carrier of H ; :: thesis: H = (Omega). (G ./. N)
then A2: the carrier of G = (nat_hom N9) " the carrier of H9 by Def20;

now :: thesis: for h being Element of (G ./. N9) holds
( ( h in H9 implies h in (Omega). (G ./. N9) ) & ( h in (Omega). (G ./. N9) implies h in H9 ) )

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

end;

then H9 = (Omega). (G ./. N9) ;
then the carrier of H = Cosets N by Def14;
hence H = (Omega). (G ./. N) by Lm4; :: thesis: verum