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 N = () " the carrier of H holds
H = (1). (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 N = () " the carrier of H holds
H = (1). (G ./. N)

let N be strict normal StableSubgroup of G; :: thesis: for H being strict StableSubgroup of G ./. N st the carrier of N = () " the carrier of H holds
H = (1). (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 N = () " the carrier of H implies H = (1). (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 ;
then reconsider H9 = H9 as strict Subgroup of G ./. N9 by ;
assume the carrier of N = () " the carrier of H ; :: thesis: H = (1). (G ./. N)
then A2: the carrier of N9 = (nat_hom N9) " the carrier of H9 by Def20;
assume not H = (1). (G ./. N) ; :: thesis: contradiction
then not the carrier of H = {(1_ (G ./. N))} by Def8;
then consider h being object such that
A3: ( ( h in the carrier of H & not h in {(1_ (G ./. N))} ) or ( h in {(1_ (G ./. N))} & not h in the carrier of H ) ) by TARSKI:2;
per cases ( ( h in the carrier of H & not h in {(1_ (G ./. N))} ) or ( not h in the carrier of H & h in {(1_ (G ./. N))} ) ) by A3;
suppose A4: ( h in the carrier of H & not h in {(1_ (G ./. N))} ) ; :: thesis: contradiction
then {h} c= the carrier of H by ZFMISC_1:31;
then A5: (nat_hom N9) " {h} c= the carrier of N9 by ;
A6: rng (nat_hom N9) = the carrier of (Image (nat_hom N9)) by GROUP_6:44
.= the carrier of (G ./. N9) by GROUP_6:48 ;
the carrier of H9 c= the carrier of (G ./. N9) by GROUP_2:def 5;
then consider x being object such that
A7: x in dom (nat_hom N9) and
A8: (nat_hom N9) . x = h by ;
(nat_hom N9) . x in {h} by ;
then x in (nat_hom N9) " {h} by ;
then A9: x in N9 by ;
h <> 1_ (G ./. N) by ;
then A10: h <> carr N by Th43;
reconsider x = x as Element of G by A7;
x * N9 = h by ;
hence contradiction by A10, A9, GROUP_2:113; :: thesis: verum
end;
suppose ( not h in the carrier of H & h in {(1_ (G ./. N))} ) ; :: thesis: contradiction
then ( h = 1_ (G ./. N) & not h in H ) by ;
hence contradiction by Lm17; :: thesis: verum
end;
end;