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;

then the carrier of H = Cosets N by Def14;

hence H = (Omega). (G ./. N) by Lm4; :: thesis: verum

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 ) )

then
H9 = (Omega). (G ./. N9)
;( ( 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;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

then the carrier of H = Cosets N by Def14;

hence H = (Omega). (G ./. N) by Lm4; :: thesis: verum