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

for N being StableSubgroup of G

for H9 being strict StableSubgroup of H

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

for H9 being strict StableSubgroup of H

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

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

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) ) )

assume A1: N = Ker f ; :: thesis: ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

A2: 1_ H in H99 by GROUP_2:46;

then f . (1_ G) in H99 by Lm12;

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

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

A15: the carrier of G99 = A by A3, A10, Lm14;

take G99 ; :: thesis: ( the carrier of G99 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) ) )

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

for N being StableSubgroup of G

for H9 being strict StableSubgroup of H

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

for H9 being strict StableSubgroup of H

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

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

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) ) )

assume A1: N = Ker f ; :: thesis: ex G9 being strict StableSubgroup of G st

( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

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

A2: 1_ H in H99 by GROUP_2:46;

then f . (1_ G) in H99 by Lm12;

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

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

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

x in the carrier of G

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

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

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

then ex g being Element of G st

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

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

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

then ex g being Element of G st

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

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

A3: now :: thesis: for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A

g1 * g2 in A

let g1, g2 be Element of G; :: thesis: ( g1 in A & g2 in A implies g1 * g2 in A )

assume that

A4: g1 in A and

A5: g2 in A ; :: thesis: g1 * g2 in A

consider b being Element of G such that

A6: b = g2 and

A7: f . b in H99 by A5;

consider a being Element of G such that

A8: a = g1 and

A9: f . a in H99 by A4;

set fb = f . b;

set fa = f . a;

( f . (a * b) = (f . a) * (f . b) & (f . a) * (f . b) in H99 ) by A9, A7, GROUP_2:50, GROUP_6:def 6;

hence g1 * g2 in A by A8, A6; :: thesis: verum

end;assume that

A4: g1 in A and

A5: g2 in A ; :: thesis: g1 * g2 in A

consider b being Element of G such that

A6: b = g2 and

A7: f . b in H99 by A5;

consider a being Element of G such that

A8: a = g1 and

A9: f . a in H99 by A4;

set fb = f . b;

set fa = f . a;

( f . (a * b) = (f . a) * (f . b) & (f . a) * (f . b) in H99 ) by A9, A7, GROUP_2:50, GROUP_6:def 6;

hence g1 * g2 in A by A8, A6; :: thesis: verum

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

for g being Element of G st g in A holds

(G ^ o) . g in A

for g being Element of G st g in A holds

(G ^ o) . g in A

let o be Element of O; :: thesis: for g being Element of G st g in A holds

(G ^ o) . g in A

let g be Element of G; :: thesis: ( g in A implies (G ^ o) . g in A )

assume g in A ; :: thesis: (G ^ o) . g in A

then consider a being Element of G such that

A11: a = g and

A12: f . a in H99 ;

f . a in the carrier of H99 by A12, STRUCT_0:def 5;

then f . a in H9 by STRUCT_0:def 5;

then (H ^ o) . (f . g) in H9 by A11, Lm9;

then f . ((G ^ o) . g) in H9 by Def18;

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

then f . ((G ^ o) . g) in H99 by STRUCT_0:def 5;

hence (G ^ o) . g in A ; :: thesis: verum

end;(G ^ o) . g in A

let g be Element of G; :: thesis: ( g in A implies (G ^ o) . g in A )

assume g in A ; :: thesis: (G ^ o) . g in A

then consider a being Element of G such that

A11: a = g and

A12: f . a in H99 ;

f . a in the carrier of H99 by A12, STRUCT_0:def 5;

then f . a in H9 by STRUCT_0:def 5;

then (H ^ o) . (f . g) in H9 by A11, Lm9;

then f . ((G ^ o) . g) in H9 by Def18;

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

then f . ((G ^ o) . g) in H99 by STRUCT_0:def 5;

hence (G ^ o) . g in A ; :: thesis: verum

now :: thesis: for g being Element of G st g in A holds

g " in A

then consider G99 being strict StableSubgroup of G such that g " in A

let g be Element of G; :: thesis: ( g in A implies g " in A )

assume g in A ; :: thesis: g " in A

then consider a being Element of G such that

A13: a = g and

A14: f . a in H99 ;

(f . a) " in H99 by A14, GROUP_2:51;

then f . (a ") in H99 by Lm13;

hence g " in A by A13; :: thesis: verum

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

then consider a being Element of G such that

A13: a = g and

A14: f . a in H99 ;

(f . a) " in H99 by A14, GROUP_2:51;

then f . (a ") in H99 by Lm13;

hence g " in A by A13; :: thesis: verum

A15: the carrier of G99 = A by A3, A10, Lm14;

take G99 ; :: thesis: ( the carrier of G99 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) ) )

now :: thesis: for g being Element of G holds

( ( g in A implies g in f " the carrier of H9 ) & ( g in f " the carrier of H9 implies g in A ) )

hence
the carrier of G99 = f " the carrier of H9
by A15, SUBSET_1:3; :: thesis: ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) )( ( g in A implies g in f " the carrier of H9 ) & ( g in f " the carrier of H9 implies g in A ) )

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

let g be Element of G; :: thesis: ( ( g in A implies g in f " the carrier of H9 ) & ( g in f " the carrier of H9 implies g in A ) )

then consider h being Element of H such that

A17: ( [g,h] in R & h in the carrier of H9 ) by RELSET_1:30;

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

hence g in A ; :: thesis: verum

end;let g be Element of G; :: thesis: ( ( g in A implies g in f " the carrier of H9 ) & ( g in f " the carrier of H9 implies g in A ) )

hereby :: thesis: ( g in f " the carrier of H9 implies g in A )

assume
g in f " the carrier of H9
; :: thesis: g in Aassume
g in A
; :: thesis: g in f " the carrier of H9

then ex a being Element of G st

( a = g & f . a in H99 ) ;

then A16: f . g in the carrier of H9 by STRUCT_0:def 5;

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

then [g,(f . g)] in f by FUNCT_1:1;

hence g in f " the carrier of H9 by A16, RELSET_1:30; :: thesis: verum

end;then ex a being Element of G st

( a = g & f . a in H99 ) ;

then A16: f . g in the carrier of H9 by STRUCT_0:def 5;

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

then [g,(f . g)] in f by FUNCT_1:1;

hence g in f " the carrier of H9 by A16, RELSET_1:30; :: thesis: verum

then consider h being Element of H such that

A17: ( [g,h] in R & h in the carrier of H9 ) by RELSET_1:30;

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

hence g in A ; :: thesis: verum

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

now :: thesis: ( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) )

hence
( H9 is normal implies ( N is normal StableSubgroup of G99 & G99 is normal ) )
; :: thesis: verumassume A18:
H9 is normal
; :: thesis: ( N is normal StableSubgroup of G99 & G99 is normal )

H is normal by GROUP_3:118;

hence G99 is normal ; :: thesis: verum

end;now :: thesis: for g being Element of G st g in N holds

g in G99

hence
N is normal StableSubgroup of G99
by A1, Th13, Th40; :: thesis: G99 is normal g in G99

let g be Element of G; :: thesis: ( g in N implies g in G99 )

assume g in N ; :: thesis: g in G99

then f . g = 1_ H by A1, Th47;

then g in the carrier of G99 by A2, A15;

hence g in G99 by STRUCT_0:def 5; :: thesis: verum

end;assume g in N ; :: thesis: g in G99

then f . g = 1_ H by A1, Th47;

then g in the carrier of G99 by A2, A15;

hence g in G99 by STRUCT_0:def 5; :: thesis: verum

now :: thesis: for g being Element of G holds g * G9 c= G9 * g

then
for H being strict Subgroup of G st H = multMagma(# the carrier of G99, the multF of G99 #) holds let g be Element of G; :: thesis: g * G9 c= G9 * g

end;now :: thesis: for x being object st x in g * G9 holds

x in G9 * g

hence
g * G9 c= G9 * g
; :: thesis: verumx in G9 * g

H99 is normal
by A18;

then A19: H99 |^ ((f . g) ") = H99 by GROUP_3:def 13;

let x be object ; :: thesis: ( x in g * G9 implies x in G9 * g )

assume x in g * G9 ; :: thesis: x in G9 * g

then consider h being Element of G such that

A20: x = g * h and

A21: h in A by A15, GROUP_2:27;

set h9 = (g * h) * (g ");

A22: f . ((g * h) * (g ")) = (f . (g * h)) * (f . (g ")) by GROUP_6:def 6

.= ((f . g) * (f . h)) * (f . (g ")) by GROUP_6:def 6

.= ((((f . g) ") ") * (f . h)) * ((f . g) ") by Lm13

.= (f . h) |^ ((f . g) ") by GROUP_3:def 2 ;

ex a being Element of G st

( a = h & f . a in H99 ) by A21;

then f . ((g * h) * (g ")) in H99 by A19, A22, GROUP_3:58;

then A23: (g * h) * (g ") in A ;

((g * h) * (g ")) * g = (g * h) * ((g ") * g) by GROUP_1:def 3

.= (g * h) * (1_ G) by GROUP_1:def 5

.= x by A20, GROUP_1:def 4 ;

hence x in G9 * g by A15, A23, GROUP_2:28; :: thesis: verum

end;then A19: H99 |^ ((f . g) ") = H99 by GROUP_3:def 13;

let x be object ; :: thesis: ( x in g * G9 implies x in G9 * g )

assume x in g * G9 ; :: thesis: x in G9 * g

then consider h being Element of G such that

A20: x = g * h and

A21: h in A by A15, GROUP_2:27;

set h9 = (g * h) * (g ");

A22: f . ((g * h) * (g ")) = (f . (g * h)) * (f . (g ")) by GROUP_6:def 6

.= ((f . g) * (f . h)) * (f . (g ")) by GROUP_6:def 6

.= ((((f . g) ") ") * (f . h)) * ((f . g) ") by Lm13

.= (f . h) |^ ((f . g) ") by GROUP_3:def 2 ;

ex a being Element of G st

( a = h & f . a in H99 ) by A21;

then f . ((g * h) * (g ")) in H99 by A19, A22, GROUP_3:58;

then A23: (g * h) * (g ") in A ;

((g * h) * (g ")) * g = (g * h) * ((g ") * g) by GROUP_1:def 3

.= (g * h) * (1_ G) by GROUP_1:def 5

.= x by A20, GROUP_1:def 4 ;

hence x in G9 * g by A15, A23, GROUP_2:28; :: thesis: verum

H is normal by GROUP_3:118;

hence G99 is normal ; :: thesis: verum