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 = (nat_hom 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 = (nat_hom 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 = (nat_hom 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 = (nat_hom 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 Def14, Def15;

then reconsider H9 = H9 as strict Subgroup of G ./. N9 by A1, GROUP_2:def 5;

assume the carrier of N = (nat_hom 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;

for N being strict normal StableSubgroup of G

for H being strict StableSubgroup of G ./. N st the carrier of N = (nat_hom 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 = (nat_hom 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 = (nat_hom 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 = (nat_hom 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 Def14, Def15;

then reconsider H9 = H9 as strict Subgroup of G ./. N9 by A1, GROUP_2:def 5;

assume the carrier of N = (nat_hom 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;

end;

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 A2, RELAT_1:143;

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 A4, A6, FUNCT_1:def 3;

(nat_hom N9) . x in {h} by A8, TARSKI:def 1;

then x in (nat_hom N9) " {h} by A7, FUNCT_1:def 7;

then A9: x in N9 by A5, STRUCT_0:def 5;

h <> 1_ (G ./. N) by A4, TARSKI:def 1;

then A10: h <> carr N by Th43;

reconsider x = x as Element of G by A7;

x * N9 = h by A8, GROUP_6:def 8;

hence contradiction by A10, A9, GROUP_2:113; :: thesis: verum

end;then A5: (nat_hom N9) " {h} c= the carrier of N9 by A2, RELAT_1:143;

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 A4, A6, FUNCT_1:def 3;

(nat_hom N9) . x in {h} by A8, TARSKI:def 1;

then x in (nat_hom N9) " {h} by A7, FUNCT_1:def 7;

then A9: x in N9 by A5, STRUCT_0:def 5;

h <> 1_ (G ./. N) by A4, TARSKI:def 1;

then A10: h <> carr N by Th43;

reconsider x = x as Element of G by A7;

x * N9 = h by A8, GROUP_6:def 8;

hence contradiction by A10, A9, GROUP_2:113; :: thesis: verum

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 STRUCT_0:def 5, TARSKI:def 1;

hence contradiction by Lm17; :: thesis: verum

end;hence contradiction by Lm17; :: thesis: verum