let O be set ; :: thesis: for G, H being GroupWithOperators of O

for N being StableSubgroup of G

for G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

let G, H be GroupWithOperators of O; :: thesis: for N being StableSubgroup of G

for G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

let N be StableSubgroup of G; :: thesis: for G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by Lm15;

let G9 be strict StableSubgroup of G; :: thesis: for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

reconsider G99 = multMagma(# the carrier of G9, the multF of G9 #) as strict Subgroup of G by Lm15;

let f be Homomorphism of G,H; :: thesis: ( N = Ker f implies ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) ) )

set A = { (f . g) where g is Element of G : g in G99 } ;

A1: ( G99 * N9 = G9 * N & N9 * G99 = N * G9 ) ;

1_ G in G99 by GROUP_2:46;

then f . (1_ G) in { (f . g) where g is Element of G : g in G99 } ;

then reconsider A = { (f . g) where g is Element of G : g in G99 } as non empty set ;

A12: the carrier of H99 = A by A2, A7, Lm14;

assume A13: N = Ker f ; :: thesis: ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

then N9 is normal by Def10;

then A14: (carr G99) * N9 = N9 * (carr G99) by GROUP_3:120;

reconsider H9 = multMagma(# the carrier of H99, the multF of H99 #) as strict Subgroup of H by Lm15;

take H99 ; :: thesis: ( the carrier of H99 = f .: the carrier of G9 & f " the carrier of H99 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H99 is normal ) )

hence f " the carrier of H99 = the carrier of (G9 "\/" N) by A14, A1, Th30; :: thesis: ( f is onto & G9 is normal implies H99 is normal )

for N being StableSubgroup of G

for G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

let G, H be GroupWithOperators of O; :: thesis: for N being StableSubgroup of G

for G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

let N be StableSubgroup of G; :: thesis: for G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by Lm15;

let G9 be strict StableSubgroup of G; :: thesis: for f being Homomorphism of G,H st N = Ker f holds

ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

reconsider G99 = multMagma(# the carrier of G9, the multF of G9 #) as strict Subgroup of G by Lm15;

let f be Homomorphism of G,H; :: thesis: ( N = Ker f implies ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) ) )

set A = { (f . g) where g is Element of G : g in G99 } ;

A1: ( G99 * N9 = G9 * N & N9 * G99 = N * G9 ) ;

1_ G in G99 by GROUP_2:46;

then f . (1_ G) in { (f . g) where g is Element of G : g in G99 } ;

then reconsider A = { (f . g) where g is Element of G : g in G99 } as non empty set ;

now :: thesis: for x being object st x in A holds

x in the carrier of H

then reconsider A = A as Subset of H by TARSKI:def 3;x in the carrier of H

let x be object ; :: thesis: ( x in A implies x in the carrier of H )

assume x in A ; :: thesis: x in the carrier of H

then ex g being Element of G st

( x = f . g & g in G99 ) ;

hence x in the carrier of H ; :: thesis: verum

end;assume x in A ; :: thesis: x in the carrier of H

then ex g being Element of G st

( x = f . g & g in G99 ) ;

hence x in the carrier of H ; :: thesis: verum

A2: now :: thesis: for h1, h2 being Element of H st h1 in A & h2 in A holds

h1 * h2 in A

h1 * h2 in A

let h1, h2 be Element of H; :: thesis: ( h1 in A & h2 in A implies h1 * h2 in A )

assume that

A3: h1 in A and

A4: h2 in A ; :: thesis: h1 * h2 in A

consider a being Element of G such that

A5: ( h1 = f . a & a in G99 ) by A3;

consider b being Element of G such that

A6: ( h2 = f . b & b in G99 ) by A4;

( f . (a * b) = h1 * h2 & a * b in G99 ) by A5, A6, GROUP_2:50, GROUP_6:def 6;

hence h1 * h2 in A ; :: thesis: verum

end;assume that

A3: h1 in A and

A4: h2 in A ; :: thesis: h1 * h2 in A

consider a being Element of G such that

A5: ( h1 = f . a & a in G99 ) by A3;

consider b being Element of G such that

A6: ( h2 = f . b & b in G99 ) by A4;

( f . (a * b) = h1 * h2 & a * b in G99 ) by A5, A6, GROUP_2:50, GROUP_6:def 6;

hence h1 * h2 in A ; :: thesis: verum

A7: now :: thesis: for o being Element of O

for h being Element of H st h in A holds

(H ^ o) . h in A

for h being Element of H st h in A holds

(H ^ o) . h in A

let o be Element of O; :: thesis: for h being Element of H st h in A holds

(H ^ o) . h in A

let h be Element of H; :: thesis: ( h in A implies (H ^ o) . h in A )

assume h in A ; :: thesis: (H ^ o) . h in A

then consider g being Element of G such that

A8: h = f . g and

A9: g in G99 ;

g in the carrier of G99 by A9, STRUCT_0:def 5;

then g in G9 by STRUCT_0:def 5;

then (G ^ o) . g in G9 by Lm9;

then (G ^ o) . g in the carrier of G9 by STRUCT_0:def 5;

then A10: (G ^ o) . g in G99 by STRUCT_0:def 5;

(H ^ o) . h = f . ((G ^ o) . g) by A8, Def18;

hence (H ^ o) . h in A by A10; :: thesis: verum

end;(H ^ o) . h in A

let h be Element of H; :: thesis: ( h in A implies (H ^ o) . h in A )

assume h in A ; :: thesis: (H ^ o) . h in A

then consider g being Element of G such that

A8: h = f . g and

A9: g in G99 ;

g in the carrier of G99 by A9, STRUCT_0:def 5;

then g in G9 by STRUCT_0:def 5;

then (G ^ o) . g in G9 by Lm9;

then (G ^ o) . g in the carrier of G9 by STRUCT_0:def 5;

then A10: (G ^ o) . g in G99 by STRUCT_0:def 5;

(H ^ o) . h = f . ((G ^ o) . g) by A8, Def18;

hence (H ^ o) . h in A by A10; :: thesis: verum

now :: thesis: for h being Element of H st h in A holds

h " in A

then consider H99 being strict StableSubgroup of H such that h " in A

let h be Element of H; :: thesis: ( h in A implies h " in A )

assume h in A ; :: thesis: h " in A

then consider g being Element of G such that

A11: ( h = f . g & g in G99 ) ;

( g " in G99 & h " = f . (g ") ) by A11, Lm13, GROUP_2:51;

hence h " in A ; :: thesis: verum

end;assume h in A ; :: thesis: h " in A

then consider g being Element of G such that

A11: ( h = f . g & g in G99 ) ;

( g " in G99 & h " = f . (g ") ) by A11, Lm13, GROUP_2:51;

hence h " in A ; :: thesis: verum

A12: the carrier of H99 = A by A2, A7, Lm14;

assume A13: N = Ker f ; :: thesis: ex H9 being strict StableSubgroup of H st

( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

then N9 is normal by Def10;

then A14: (carr G99) * N9 = N9 * (carr G99) by GROUP_3:120;

reconsider H9 = multMagma(# the carrier of H99, the multF of H99 #) as strict Subgroup of H by Lm15;

take H99 ; :: thesis: ( the carrier of H99 = f .: the carrier of G9 & f " the carrier of H99 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H99 is normal ) )

A15: now :: thesis: for h being Element of H holds

( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )

hence A20:
the carrier of H99 = f .: the carrier of G9
by A12, SUBSET_1:3; :: thesis: ( f " the carrier of H99 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H99 is normal ) )( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )

reconsider R = f as Relation of the carrier of G, the carrier of H ;

let h be Element of H; :: thesis: ( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )

then consider g being Element of G such that

A19: ( [g,h] in R & g in the carrier of G9 ) by RELSET_1:29;

( f . g = h & g in G99 ) by A19, FUNCT_1:1, STRUCT_0:def 5;

hence h in A ; :: thesis: verum

end;let h be Element of H; :: thesis: ( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )

hereby :: thesis: ( h in f .: the carrier of G9 implies h in A )

assume
h in f .: the carrier of G9
; :: thesis: h in Aassume
h in A
; :: thesis: h in f .: the carrier of G9

then consider g being Element of G such that

A16: h = f . g and

A17: g in G99 ;

A18: g in the carrier of G9 by A17, STRUCT_0:def 5;

dom f = the carrier of G by FUNCT_2:def 1;

then [g,h] in f by A16, FUNCT_1:1;

hence h in f .: the carrier of G9 by A18, RELSET_1:29; :: thesis: verum

end;then consider g being Element of G such that

A16: h = f . g and

A17: g in G99 ;

A18: g in the carrier of G9 by A17, STRUCT_0:def 5;

dom f = the carrier of G by FUNCT_2:def 1;

then [g,h] in f by A16, FUNCT_1:1;

hence h in f .: the carrier of G9 by A18, RELSET_1:29; :: thesis: verum

then consider g being Element of G such that

A19: ( [g,h] in R & g in the carrier of G9 ) by RELSET_1:29;

( f . g = h & g in G99 ) by A19, FUNCT_1:1, STRUCT_0:def 5;

hence h in A ; :: thesis: verum

A21: now :: thesis: for x being object st x in f " the carrier of H9 holds

x in G99 * N9

A27:
dom f = the carrier of G
by FUNCT_2:def 1;x in G99 * N9

let x be object ; :: thesis: ( x in f " the carrier of H9 implies x in G99 * N9 )

assume A22: x in f " the carrier of H9 ; :: thesis: x in G99 * N9

then f . x in the carrier of H9 by FUNCT_1:def 7;

then consider g1 being object such that

A23: g1 in dom f and

A24: g1 in the carrier of G9 and

A25: f . g1 = f . x by A20, FUNCT_1:def 6;

reconsider g1 = g1, g2 = x as Element of G by A22, A23;

consider g3 being Element of G such that

A26: g2 = g1 * g3 by GROUP_1:15;

f . g2 = (f . g2) * (f . g3) by A25, A26, GROUP_6:def 6;

then f . g3 = 1_ H by GROUP_1:7;

then g3 in Ker f by Th47;

then g3 in the carrier of N by A13, STRUCT_0:def 5;

hence x in G99 * N9 by A24, A26; :: thesis: verum

end;assume A22: x in f " the carrier of H9 ; :: thesis: x in G99 * N9

then f . x in the carrier of H9 by FUNCT_1:def 7;

then consider g1 being object such that

A23: g1 in dom f and

A24: g1 in the carrier of G9 and

A25: f . g1 = f . x by A20, FUNCT_1:def 6;

reconsider g1 = g1, g2 = x as Element of G by A22, A23;

consider g3 being Element of G such that

A26: g2 = g1 * g3 by GROUP_1:15;

f . g2 = (f . g2) * (f . g3) by A25, A26, GROUP_6:def 6;

then f . g3 = 1_ H by GROUP_1:7;

then g3 in Ker f by Th47;

then g3 in the carrier of N by A13, STRUCT_0:def 5;

hence x in G99 * N9 by A24, A26; :: thesis: verum

now :: thesis: for x being object st x in G99 * N9 holds

x in f " the carrier of H9

then
f " the carrier of H9 = (carr G9) * (carr N)
by A21, TARSKI:2;x in f " the carrier of H9

let x be object ; :: thesis: ( x in G99 * N9 implies x in f " the carrier of H9 )

assume A28: x in G99 * N9 ; :: thesis: x in f " the carrier of H9

then consider g1, g2 being Element of G such that

A29: x = g1 * g2 and

A30: g1 in carr G9 and

A31: g2 in carr N9 ;

A32: g2 in Ker f by A13, A31, STRUCT_0:def 5;

f . x = (f . g1) * (f . g2) by A29, GROUP_6:def 6

.= (f . g1) * (1_ H) by A32, Th47

.= f . g1 by GROUP_1:def 4 ;

then f . x in f .: the carrier of G9 by A27, A30, FUNCT_1:def 6;

then x in f " (f .: the carrier of G9) by A27, A28, FUNCT_1:def 7;

hence x in f " the carrier of H9 by A12, A15, SUBSET_1:3; :: thesis: verum

end;assume A28: x in G99 * N9 ; :: thesis: x in f " the carrier of H9

then consider g1, g2 being Element of G such that

A29: x = g1 * g2 and

A30: g1 in carr G9 and

A31: g2 in carr N9 ;

A32: g2 in Ker f by A13, A31, STRUCT_0:def 5;

f . x = (f . g1) * (f . g2) by A29, GROUP_6:def 6

.= (f . g1) * (1_ H) by A32, Th47

.= f . g1 by GROUP_1:def 4 ;

then f . x in f .: the carrier of G9 by A27, A30, FUNCT_1:def 6;

then x in f " (f .: the carrier of G9) by A27, A28, FUNCT_1:def 7;

hence x in f " the carrier of H9 by A12, A15, SUBSET_1:3; :: thesis: verum

hence f " the carrier of H99 = the carrier of (G9 "\/" N) by A14, A1, Th30; :: thesis: ( f is onto & G9 is normal implies H99 is normal )

now :: thesis: ( f is onto & G9 is normal implies H99 is normal )

hence
( f is onto & G9 is normal implies H99 is normal )
; :: thesis: verumassume that

A33: f is onto and

A34: G9 is normal ; :: thesis: H99 is normal

A35: G99 is normal by A34;

H1 is normal by GROUP_3:118;

hence H99 is normal ; :: thesis: verum

end;A33: f is onto and

A34: G9 is normal ; :: thesis: H99 is normal

A35: G99 is normal by A34;

now :: thesis: for h1 being Element of H holds h1 * H9 c= H9 * h1

then
for H1 being strict Subgroup of H st H1 = multMagma(# the carrier of H99, the multF of H99 #) holds let h1 be Element of H; :: thesis: h1 * H9 c= H9 * h1

end;now :: thesis: for x being object st x in h1 * H9 holds

x in H9 * h1

hence
h1 * H9 c= H9 * h1
; :: thesis: verumx in H9 * h1

let x be object ; :: thesis: ( x in h1 * H9 implies x in H9 * h1 )

assume x in h1 * H9 ; :: thesis: x in H9 * h1

then consider h2 being Element of H such that

A36: x = h1 * h2 and

A37: h2 in A by A12, GROUP_2:27;

set h29 = (h1 * h2) * (h1 ");

h2 in f .: the carrier of G9 by A15, A37;

then consider g2 being object such that

A38: g2 in dom f and

A39: g2 in the carrier of G99 and

A40: f . g2 = h2 by FUNCT_1:def 6;

rng f = the carrier of H by A33;

then consider g1 being object such that

A41: g1 in dom f and

A42: h1 = f . g1 by FUNCT_1:def 3;

reconsider g1 = g1, g2 = g2 as Element of G by A38, A41;

set g29 = (g1 * g2) * (g1 ");

(g1 * g2) * (g1 ") = (((g1 ") ") * g2) * (g1 ") ;

then A43: (g1 * g2) * (g1 ") = g2 |^ (g1 ") by GROUP_3:def 2;

g2 in G99 by A39, STRUCT_0:def 5;

then (g1 * g2) * (g1 ") in G99 |^ (g1 ") by A43, GROUP_3:58;

then A44: (g1 * g2) * (g1 ") in the carrier of (G99 |^ (g1 ")) by STRUCT_0:def 5;

G99 |^ (g1 ") is Subgroup of G99 by A35, GROUP_3:122;

then A45: the carrier of (G99 |^ (g1 ")) c= the carrier of G99 by GROUP_2:def 5;

(h1 * h2) * (h1 ") = ((f . g1) * (f . g2)) * (f . (g1 ")) by A40, A42, Lm13

.= (f . (g1 * g2)) * (f . (g1 ")) by GROUP_6:def 6

.= f . ((g1 * g2) * (g1 ")) by GROUP_6:def 6 ;

then (h1 * h2) * (h1 ") in f .: the carrier of G99 by A27, A44, A45, FUNCT_1:def 6;

then A46: (h1 * h2) * (h1 ") in A by A15;

((h1 * h2) * (h1 ")) * h1 = (h1 * h2) * ((h1 ") * h1) by GROUP_1:def 3

.= (h1 * h2) * (1_ H) by GROUP_1:def 5

.= x by A36, GROUP_1:def 4 ;

hence x in H9 * h1 by A12, A46, GROUP_2:28; :: thesis: verum

end;assume x in h1 * H9 ; :: thesis: x in H9 * h1

then consider h2 being Element of H such that

A36: x = h1 * h2 and

A37: h2 in A by A12, GROUP_2:27;

set h29 = (h1 * h2) * (h1 ");

h2 in f .: the carrier of G9 by A15, A37;

then consider g2 being object such that

A38: g2 in dom f and

A39: g2 in the carrier of G99 and

A40: f . g2 = h2 by FUNCT_1:def 6;

rng f = the carrier of H by A33;

then consider g1 being object such that

A41: g1 in dom f and

A42: h1 = f . g1 by FUNCT_1:def 3;

reconsider g1 = g1, g2 = g2 as Element of G by A38, A41;

set g29 = (g1 * g2) * (g1 ");

(g1 * g2) * (g1 ") = (((g1 ") ") * g2) * (g1 ") ;

then A43: (g1 * g2) * (g1 ") = g2 |^ (g1 ") by GROUP_3:def 2;

g2 in G99 by A39, STRUCT_0:def 5;

then (g1 * g2) * (g1 ") in G99 |^ (g1 ") by A43, GROUP_3:58;

then A44: (g1 * g2) * (g1 ") in the carrier of (G99 |^ (g1 ")) by STRUCT_0:def 5;

G99 |^ (g1 ") is Subgroup of G99 by A35, GROUP_3:122;

then A45: the carrier of (G99 |^ (g1 ")) c= the carrier of G99 by GROUP_2:def 5;

(h1 * h2) * (h1 ") = ((f . g1) * (f . g2)) * (f . (g1 ")) by A40, A42, Lm13

.= (f . (g1 * g2)) * (f . (g1 ")) by GROUP_6:def 6

.= f . ((g1 * g2) * (g1 ")) by GROUP_6:def 6 ;

then (h1 * h2) * (h1 ") in f .: the carrier of G99 by A27, A44, A45, FUNCT_1:def 6;

then A46: (h1 * h2) * (h1 ") in A by A15;

((h1 * h2) * (h1 ")) * h1 = (h1 * h2) * ((h1 ") * h1) by GROUP_1:def 3

.= (h1 * h2) * (1_ H) by GROUP_1:def 5

.= x by A36, GROUP_1:def 4 ;

hence x in H9 * h1 by A12, A46, GROUP_2:28; :: thesis: verum

H1 is normal by GROUP_3:118;

hence H99 is normal ; :: thesis: verum