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

for N, L, G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds

( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

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

for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds

( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

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

( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

reconsider N9 = G9 /\ N as StableSubgroup of G9 by Lm33;

reconsider Gs9 = 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 & L is strict normal StableSubgroup of G9 implies ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) ) )

reconsider L99 = L as Subgroup of G by Def7;

assume A1: N = Ker f ; :: thesis: ( not L is strict normal StableSubgroup of G9 or ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) ) )

then consider H9 being strict StableSubgroup of H such that

A2: the carrier of H9 = f .: the carrier of G9 and

A3: f " the carrier of H9 = the carrier of (G9 "\/" N) and

( f is onto & G9 is normal implies H9 is normal ) by Th79;

reconsider f99 = f | the carrier of (G9 "\/" N) as Homomorphism of (G9 "\/" N),H9 by A3, Th89;

reconsider Ns = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by A1, Lm6;

(carr Gs9) * Ns = Ns * (carr Gs9) by GROUP_3:120;

then A4: G9 * N = N * G9 ;

then A20: ( f99 .: the carrier of (G9 "\/" N) = f .: the carrier of (G9 "\/" N) & the carrier of H9 = f .: the carrier of (G9 "\/" N) ) by A2, A4, Th30, RELAT_1:129;

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

then reconsider L9 = L as strict StableSubgroup of G9 ;

reconsider N1 = L "\/" N as StableSubgroup of G9 "\/" N by A29, Th38;

(carr L99) * Ns = Ns * (carr L99) by GROUP_3:120;

then A30: L * N = N * L ;

then A33: N9 = Ker f9 by Def21;

then consider H99 being strict StableSubgroup of H9 such that

A34: the carrier of H99 = f9 .: the carrier of L9 and

A35: f9 " the carrier of H99 = the carrier of (L9 "\/" N9) and

A36: ( f9 is onto & L9 is normal implies H99 is normal ) by Th79;

consider N2 being strict StableSubgroup of G9 such that

A37: the carrier of N2 = f9 " the carrier of H99 and

A38: ( H99 is normal implies ( N9 is normal StableSubgroup of N2 & N2 is normal ) ) by A33, Th78;

( f9 .: the carrier of G9 = f .: the carrier of G9 & H9 is strict StableSubgroup of H9 ) by Lm3, RELAT_1:129;

then Image f9 = H9 by A2, Def22;

then A39: rng f9 = the carrier of H9 by Th49;

then reconsider H99 = H99 as normal StableSubgroup of H9 by A29, A36;

A40: N2 = L9 "\/" N9 by A35, A37, Lm4;

hence L "\/" (G9 /\ N) is normal StableSubgroup of G9 by A29, A36, A38, A39, Th86; :: thesis: ( L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

set l = nat_hom H99;

set f1 = (nat_hom H99) * f99;

A41: N2 = L "\/" (G9 /\ N) by A40, Th86;

A42: L "\/" N is StableSubgroup of G9 "\/" N by A29, Th38;

then the carrier of L c= the carrier of G9 by GROUP_2:def 5;

then f9 .: the carrier of L = f .: the carrier of L by RELAT_1:129;

then f99 " (f9 .: the carrier of L) = L * N by A21, A43, TARSKI:2;

then A52: f99 " the carrier of H99 = the carrier of N1 by A34, A30, Th30;

A53: f99 " the carrier of (Ker (nat_hom H99)) = f99 " the carrier of H99 by Th48;

then the carrier of (Ker ((nat_hom H99) * f99)) = the carrier of N1 by A52, Th88;

hence L "\/" N is normal StableSubgroup of G9 "\/" N by Lm4; :: thesis: for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic

A54: Ker ((nat_hom H99) * f99) = N1 by A52, A53, Lm4, Th88;

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ; :: thesis: verum

for N, L, G9 being strict StableSubgroup of G

for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds

( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

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

for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds

( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

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

( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

reconsider N9 = G9 /\ N as StableSubgroup of G9 by Lm33;

reconsider Gs9 = 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 & L is strict normal StableSubgroup of G9 implies ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) ) )

reconsider L99 = L as Subgroup of G by Def7;

assume A1: N = Ker f ; :: thesis: ( not L is strict normal StableSubgroup of G9 or ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) ) )

then consider H9 being strict StableSubgroup of H such that

A2: the carrier of H9 = f .: the carrier of G9 and

A3: f " the carrier of H9 = the carrier of (G9 "\/" N) and

( f is onto & G9 is normal implies H9 is normal ) by Th79;

reconsider f99 = f | the carrier of (G9 "\/" N) as Homomorphism of (G9 "\/" N),H9 by A3, Th89;

reconsider Ns = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by A1, Lm6;

(carr Gs9) * Ns = Ns * (carr Gs9) by GROUP_3:120;

then A4: G9 * N = N * G9 ;

A5: now :: thesis: for y being object st y in f .: the carrier of G9 holds

y in f .: (G9 * N)

A12:
dom f = the carrier of G
by FUNCT_2:def 1;y in f .: (G9 * N)

let y be object ; :: thesis: ( y in f .: the carrier of G9 implies y in f .: (G9 * N) )

assume y in f .: the carrier of G9 ; :: thesis: y in f .: (G9 * N)

then consider x being object such that

A6: x in dom f and

A7: x in the carrier of G9 and

A8: y = f . x by FUNCT_1:def 6;

reconsider x = x as Element of G by A6;

consider x9 being set such that

A9: x9 = x * (1_ G) ;

A10: x9 in dom f by A6, A9, GROUP_1:def 4;

A11: y = (f . x) * (1_ H) by A8, GROUP_1:def 4

.= (f . x) * (f . (1_ G)) by Lm12

.= f . x9 by A9, GROUP_6:def 6 ;

f . (1_ G) = 1_ H by Lm12;

then 1_ G in Ker f by Th47;

then 1_ G in carr N by A1, STRUCT_0:def 5;

then x9 in G9 * N by A7, A9;

hence y in f .: (G9 * N) by A10, A11, FUNCT_1:def 6; :: thesis: verum

end;assume y in f .: the carrier of G9 ; :: thesis: y in f .: (G9 * N)

then consider x being object such that

A6: x in dom f and

A7: x in the carrier of G9 and

A8: y = f . x by FUNCT_1:def 6;

reconsider x = x as Element of G by A6;

consider x9 being set such that

A9: x9 = x * (1_ G) ;

A10: x9 in dom f by A6, A9, GROUP_1:def 4;

A11: y = (f . x) * (1_ H) by A8, GROUP_1:def 4

.= (f . x) * (f . (1_ G)) by Lm12

.= f . x9 by A9, GROUP_6:def 6 ;

f . (1_ G) = 1_ H by Lm12;

then 1_ G in Ker f by Th47;

then 1_ G in carr N by A1, STRUCT_0:def 5;

then x9 in G9 * N by A7, A9;

hence y in f .: (G9 * N) by A10, A11, FUNCT_1:def 6; :: thesis: verum

now :: thesis: for y being object st y in f .: (G9 * N) holds

y in f .: the carrier of G9

then
f .: the carrier of G9 = f .: (G9 * N)
by A5, TARSKI:2;y in f .: the carrier of G9

let y be object ; :: thesis: ( y in f .: (G9 * N) implies y in f .: the carrier of G9 )

assume y in f .: (G9 * N) ; :: thesis: y in f .: the carrier of G9

then consider x being object such that

A13: x in dom f and

A14: x in G9 * N and

A15: y = f . x by FUNCT_1:def 6;

reconsider x = x as Element of G by A13;

consider g1, g2 being Element of G such that

A16: x = g1 * g2 and

A17: g1 in carr G9 and

A18: g2 in carr N by A14;

A19: g2 in N by A18, STRUCT_0:def 5;

y = (f . g1) * (f . g2) by A15, A16, GROUP_6:def 6

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

.= f . g1 by GROUP_1:def 4 ;

hence y in f .: the carrier of G9 by A12, A17, FUNCT_1:def 6; :: thesis: verum

end;assume y in f .: (G9 * N) ; :: thesis: y in f .: the carrier of G9

then consider x being object such that

A13: x in dom f and

A14: x in G9 * N and

A15: y = f . x by FUNCT_1:def 6;

reconsider x = x as Element of G by A13;

consider g1, g2 being Element of G such that

A16: x = g1 * g2 and

A17: g1 in carr G9 and

A18: g2 in carr N by A14;

A19: g2 in N by A18, STRUCT_0:def 5;

y = (f . g1) * (f . g2) by A15, A16, GROUP_6:def 6

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

.= f . g1 by GROUP_1:def 4 ;

hence y in f .: the carrier of G9 by A12, A17, FUNCT_1:def 6; :: thesis: verum

then A20: ( f99 .: the carrier of (G9 "\/" N) = f .: the carrier of (G9 "\/" N) & the carrier of H9 = f .: the carrier of (G9 "\/" N) ) by A2, A4, Th30, RELAT_1:129;

A21: now :: thesis: for x being object st x in f99 " (f .: the carrier of L) holds

x in L * N

reconsider f9 = f | the carrier of G9 as Homomorphism of G9,H9 by A2, Th89;x in L * N

let x be object ; :: thesis: ( x in f99 " (f .: the carrier of L) implies x in L * N )

assume x in f99 " (f .: the carrier of L) ; :: thesis: x in L * N

then A22: x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by FUNCT_1:70;

then x in f " (f .: the carrier of L) by XBOOLE_0:def 4;

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

then consider g1 being object such that

A23: g1 in dom f and

A24: g1 in the carrier of L and

A25: f . x = f . g1 by 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 A1, STRUCT_0:def 5;

hence x in L * N by A24, A26; :: thesis: verum

end;assume x in f99 " (f .: the carrier of L) ; :: thesis: x in L * N

then A22: x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by FUNCT_1:70;

then x in f " (f .: the carrier of L) by XBOOLE_0:def 4;

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

then consider g1 being object such that

A23: g1 in dom f and

A24: g1 in the carrier of L and

A25: f . x = f . g1 by 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 A1, STRUCT_0:def 5;

hence x in L * N by A24, A26; :: thesis: verum

A27: now :: thesis: for x being object st x in the carrier of N9 holds

x in { a where a is Element of G9 : f9 . a = 1_ H9 }

assume A29:
L is strict normal StableSubgroup of G9
; :: thesis: ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" Nx in { a where a is Element of G9 : f9 . a = 1_ H9 }

let x be object ; :: thesis: ( x in the carrier of N9 implies x in { a where a is Element of G9 : f9 . a = 1_ H9 } )

assume x in the carrier of N9 ; :: thesis: x in { a where a is Element of G9 : f9 . a = 1_ H9 }

then A28: x in (carr G9) /\ (carr N) by Def25;

then reconsider a9 = x as Element of G9 by XBOOLE_0:def 4;

reconsider a99 = a9 as Element of G by Th2;

x in carr N by A28, XBOOLE_0:def 4;

then x in N by STRUCT_0:def 5;

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

then f . a9 = 1_ H9 by Th4;

then f9 . a9 = 1_ H9 by FUNCT_1:49;

hence x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis: verum

end;assume x in the carrier of N9 ; :: thesis: x in { a where a is Element of G9 : f9 . a = 1_ H9 }

then A28: x in (carr G9) /\ (carr N) by Def25;

then reconsider a9 = x as Element of G9 by XBOOLE_0:def 4;

reconsider a99 = a9 as Element of G by Th2;

x in carr N by A28, XBOOLE_0:def 4;

then x in N by STRUCT_0:def 5;

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

then f . a9 = 1_ H9 by Th4;

then f9 . a9 = 1_ H9 by FUNCT_1:49;

hence x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis: verum

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

then reconsider L9 = L as strict StableSubgroup of G9 ;

reconsider N1 = L "\/" N as StableSubgroup of G9 "\/" N by A29, Th38;

(carr L99) * Ns = Ns * (carr L99) by GROUP_3:120;

then A30: L * N = N * L ;

now :: thesis: for x being object st x in { a where a is Element of G9 : f9 . a = 1_ H9 } holds

x in the carrier of N9

then
the carrier of N9 = { a where a is Element of G9 : f9 . a = 1_ H9 }
by A27, TARSKI:2;x in the carrier of N9

let x be object ; :: thesis: ( x in { a where a is Element of G9 : f9 . a = 1_ H9 } implies x in the carrier of N9 )

assume x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis: x in the carrier of N9

then consider a being Element of G9 such that

A31: x = a and

A32: f9 . a = 1_ H9 ;

reconsider a = a as Element of G by Th2;

f . a = 1_ H9 by A32, FUNCT_1:49;

then f . a = 1_ H by Th4;

then x in N by A1, A31, Th47;

then x in carr N by STRUCT_0:def 5;

then x in (carr G9) /\ (carr N) by A31, XBOOLE_0:def 4;

hence x in the carrier of N9 by Def25; :: thesis: verum

end;assume x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis: x in the carrier of N9

then consider a being Element of G9 such that

A31: x = a and

A32: f9 . a = 1_ H9 ;

reconsider a = a as Element of G by Th2;

f . a = 1_ H9 by A32, FUNCT_1:49;

then f . a = 1_ H by Th4;

then x in N by A1, A31, Th47;

then x in carr N by STRUCT_0:def 5;

then x in (carr G9) /\ (carr N) by A31, XBOOLE_0:def 4;

hence x in the carrier of N9 by Def25; :: thesis: verum

then A33: N9 = Ker f9 by Def21;

then consider H99 being strict StableSubgroup of H9 such that

A34: the carrier of H99 = f9 .: the carrier of L9 and

A35: f9 " the carrier of H99 = the carrier of (L9 "\/" N9) and

A36: ( f9 is onto & L9 is normal implies H99 is normal ) by Th79;

consider N2 being strict StableSubgroup of G9 such that

A37: the carrier of N2 = f9 " the carrier of H99 and

A38: ( H99 is normal implies ( N9 is normal StableSubgroup of N2 & N2 is normal ) ) by A33, Th78;

( f9 .: the carrier of G9 = f .: the carrier of G9 & H9 is strict StableSubgroup of H9 ) by Lm3, RELAT_1:129;

then Image f9 = H9 by A2, Def22;

then A39: rng f9 = the carrier of H9 by Th49;

then reconsider H99 = H99 as normal StableSubgroup of H9 by A29, A36;

A40: N2 = L9 "\/" N9 by A35, A37, Lm4;

hence L "\/" (G9 /\ N) is normal StableSubgroup of G9 by A29, A36, A38, A39, Th86; :: thesis: ( L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

set l = nat_hom H99;

set f1 = (nat_hom H99) * f99;

A41: N2 = L "\/" (G9 /\ N) by A40, Th86;

A42: L "\/" N is StableSubgroup of G9 "\/" N by A29, Th38;

A43: now :: thesis: for x being object st x in L * N holds

x in f99 " (f .: the carrier of L)

L is Subgroup of G9
by A29, Def7;x in f99 " (f .: the carrier of L)

let x be object ; :: thesis: ( x in L * N implies x in f99 " (f .: the carrier of L) )

assume A44: x in L * N ; :: thesis: x in f99 " (f .: the carrier of L)

then consider g1, g2 being Element of G such that

A45: x = g1 * g2 and

A46: g1 in carr L and

A47: g2 in carr N ;

A48: g2 in N by A47, STRUCT_0:def 5;

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

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

.= f . g1 by GROUP_1:def 4 ;

then A49: f . x in f .: the carrier of L by A12, A46, FUNCT_1:def 6;

L "\/" N is Subgroup of G9 "\/" N by A42, Def7;

then A50: the carrier of (L "\/" N) c= the carrier of (G9 "\/" N) by GROUP_2:def 5;

A51: x in the carrier of (L "\/" N) by A30, A44, Th30;

then x in G9 "\/" N by A50, STRUCT_0:def 5;

then x in G by Th1;

then x in dom f by A12, STRUCT_0:def 5;

then x in f " (f .: the carrier of L) by A49, FUNCT_1:def 7;

then x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by A51, A50, XBOOLE_0:def 4;

hence x in f99 " (f .: the carrier of L) by FUNCT_1:70; :: thesis: verum

end;assume A44: x in L * N ; :: thesis: x in f99 " (f .: the carrier of L)

then consider g1, g2 being Element of G such that

A45: x = g1 * g2 and

A46: g1 in carr L and

A47: g2 in carr N ;

A48: g2 in N by A47, STRUCT_0:def 5;

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

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

.= f . g1 by GROUP_1:def 4 ;

then A49: f . x in f .: the carrier of L by A12, A46, FUNCT_1:def 6;

L "\/" N is Subgroup of G9 "\/" N by A42, Def7;

then A50: the carrier of (L "\/" N) c= the carrier of (G9 "\/" N) by GROUP_2:def 5;

A51: x in the carrier of (L "\/" N) by A30, A44, Th30;

then x in G9 "\/" N by A50, STRUCT_0:def 5;

then x in G by Th1;

then x in dom f by A12, STRUCT_0:def 5;

then x in f " (f .: the carrier of L) by A49, FUNCT_1:def 7;

then x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by A51, A50, XBOOLE_0:def 4;

hence x in f99 " (f .: the carrier of L) by FUNCT_1:70; :: thesis: verum

then the carrier of L c= the carrier of G9 by GROUP_2:def 5;

then f9 .: the carrier of L = f .: the carrier of L by RELAT_1:129;

then f99 " (f9 .: the carrier of L) = L * N by A21, A43, TARSKI:2;

then A52: f99 " the carrier of H99 = the carrier of N1 by A34, A30, Th30;

A53: f99 " the carrier of (Ker (nat_hom H99)) = f99 " the carrier of H99 by Th48;

then the carrier of (Ker ((nat_hom H99) * f99)) = the carrier of N1 by A52, Th88;

hence L "\/" N is normal StableSubgroup of G9 "\/" N by Lm4; :: thesis: for N1 being strict normal StableSubgroup of G9 "\/" N

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic

A54: Ker ((nat_hom H99) * f99) = N1 by A52, A53, Lm4, Th88;

now :: thesis: for N19 being strict normal StableSubgroup of G9 "\/" N

for N29 being strict normal StableSubgroup of G9 st N19 = L "\/" N & N29 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic

hence
for N1 being strict normal StableSubgroup of G9 "\/" Nfor N29 being strict normal StableSubgroup of G9 st N19 = L "\/" N & N29 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic

set f2 = (nat_hom H99) * f9;

let N19 be strict normal StableSubgroup of G9 "\/" N; :: thesis: for N29 being strict normal StableSubgroup of G9 st N19 = L "\/" N & N29 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic

let N29 be strict normal StableSubgroup of G9; :: thesis: ( N19 = L "\/" N & N29 = L "\/" (G9 /\ N) implies (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic )

assume A55: N19 = L "\/" N ; :: thesis: ( N29 = L "\/" (G9 /\ N) implies (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic )

( f99 .: the carrier of (G9 "\/" N) = f9 .: the carrier of G9 & ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = (nat_hom H99) .: (f99 .: the carrier of (G9 "\/" N)) ) by A2, A20, RELAT_1:126, RELAT_1:129;

then A56: ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = ((nat_hom H99) * f9) .: the carrier of G9 by RELAT_1:126;

A57: f9 " the carrier of (Ker (nat_hom H99)) = f9 " the carrier of H99 by Th48;

assume N29 = L "\/" (G9 /\ N) ; :: thesis: (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic

then A58: N29 = Ker ((nat_hom H99) * f9) by A37, A41, A57, Lm4, Th88;

the carrier of (Image ((nat_hom H99) * f99)) = ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) by Def22

.= the carrier of (Image ((nat_hom H99) * f9)) by A56, Def22 ;

then A59: Image ((nat_hom H99) * f99) = Image ((nat_hom H99) * f9) by Lm4;

( (G9 "\/" N) ./. (Ker ((nat_hom H99) * f99)), Image ((nat_hom H99) * f99) are_isomorphic & Image ((nat_hom H99) * f9),G9 ./. (Ker ((nat_hom H99) * f9)) are_isomorphic ) by Th59;

hence (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic by A54, A55, A59, A58, Th55; :: thesis: verum

end;let N19 be strict normal StableSubgroup of G9 "\/" N; :: thesis: for N29 being strict normal StableSubgroup of G9 st N19 = L "\/" N & N29 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic

let N29 be strict normal StableSubgroup of G9; :: thesis: ( N19 = L "\/" N & N29 = L "\/" (G9 /\ N) implies (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic )

assume A55: N19 = L "\/" N ; :: thesis: ( N29 = L "\/" (G9 /\ N) implies (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic )

( f99 .: the carrier of (G9 "\/" N) = f9 .: the carrier of G9 & ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = (nat_hom H99) .: (f99 .: the carrier of (G9 "\/" N)) ) by A2, A20, RELAT_1:126, RELAT_1:129;

then A56: ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = ((nat_hom H99) * f9) .: the carrier of G9 by RELAT_1:126;

A57: f9 " the carrier of (Ker (nat_hom H99)) = f9 " the carrier of H99 by Th48;

assume N29 = L "\/" (G9 /\ N) ; :: thesis: (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic

then A58: N29 = Ker ((nat_hom H99) * f9) by A37, A41, A57, Lm4, Th88;

the carrier of (Image ((nat_hom H99) * f99)) = ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) by Def22

.= the carrier of (Image ((nat_hom H99) * f9)) by A56, Def22 ;

then A59: Image ((nat_hom H99) * f99) = Image ((nat_hom H99) * f9) by Lm4;

( (G9 "\/" N) ./. (Ker ((nat_hom H99) * f99)), Image ((nat_hom H99) * f99) are_isomorphic & Image ((nat_hom H99) * f9),G9 ./. (Ker ((nat_hom H99) * f9)) are_isomorphic ) by Th59;

hence (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic by A54, A55, A59, A58, Th55; :: thesis: verum

for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds

(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ; :: thesis: verum