let O be set ; :: thesis:
let G, H be strict GroupWithOperators of O; :: thesis:
let N, L, G9 be strict StableSubgroup of G; :: thesis:
reconsider N9 = G9 /\ N as StableSubgroup of G9 by Lm34;
reconsider Gs9 = multMagma(# the carrier of G9,the multF of G9 #) as strict Subgroup of G by Lm16;
let f be Homomorphism of G,H; :: thesis:
reconsider L99 = L as Subgroup of G by Def7;
assume A1: N = Ker f ; :: thesis:
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, Lm7;
(carr Gs9) * Ns = Ns * (carr Gs9) by GROUP_3:143;
then A4: G9 * N = N * G9 ;

A5: now

let y be set ; :: thesis:
assume y in f .: the carrier of G9 ; :: thesis:
then consider x being set such that
A6: x in dom f and
A7: x in the carrier of G9 and
A8: y = f . x by FUNCT_1:def 12;
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 5;
A11: y = (f . x) * (1_ H) by A8, GROUP_1:def 5
.= (f . x) * (f . (1_ G)) by Lm13
.= f . x9 by A9, GROUP_6:def 7 ;
f . (1_ G) = 1_ H by Lm13;
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 12; :: thesis:

end;

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

now

let y be set ; :: thesis:
assume y in f .: (G9 * N) ; :: thesis:
then consider x being set such that
A13: x in dom f and
A14: x in G9 * N and
A15: y = f . x by FUNCT_1:def 12;
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 7
.= (f . g1) * (1_ H) by A1, A19, Th47
.= f . g1 by GROUP_1:def 5 ;
hence y in f .: the carrier of G9 by A12, A17, FUNCT_1:def 12; :: thesis:

end;

then f .: the carrier of G9 = f .: (G9 * N) by A5, TARSKI:2;
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:162;

A21: now

let x be set ; :: thesis:
assume x in f99 " (f .: the carrier of L) ; :: thesis:
then A22: x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by FUNCT_1:139;
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 13;
then consider g1 being set 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 12;
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:23;
f . g2 = (f . g2) * (f . g3) by A25, A26, GROUP_6:def 7;
then f . g3 = 1_ H by GROUP_1:15;
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:

end;

reconsider f9 = f | the carrier of G9 as Homomorphism of G9,H9 by A2, Th89;

A27: now

let x be set ; :: thesis:
assume x in the carrier of N9 ; :: thesis:
then A28: x in (carr G9) /\ (carr N) by Def28;
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:72;
hence x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis:

end;

assume A29: L is strict normal StableSubgroup of G9 ; :: thesis:
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:143;
then A30: L * N = N * L ;

now

let x be set ; :: thesis:
assume x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis:
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:72;
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 Def28; :: thesis:

end;

then the carrier of N9 = { a where a is Element of G9 : f9 . a = 1_ H9 } by A27, TARSKI:2;
then A33: N9 = Ker f9 by Def24;
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 Lm4, RELAT_1:162;
then Image f9 = H9 by A2, Def25;
then A39: rng f9 = the carrier of H9 by Th49;
then reconsider H99 = H99 as normal StableSubgroup of H9 by A29, A36, FUNCT_2:def 3;
A40: N2 = L9 "\/" N9 by A35, A37, Lm5;
hence L "\/" (G9 /\ N) is normal StableSubgroup of G9 by A29, A36, A38, A39, Th86, FUNCT_2:def 3; :: thesis:
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

let x be set ; :: thesis:
assume A44: x in L * N ; :: thesis:
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 7
.= (f . g1) * (1_ H) by A1, A48, Th47
.= f . g1 by GROUP_1:def 5 ;
then A49: f . x in f .: the carrier of L by A12, A46, FUNCT_1:def 12;
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 13;
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:139; :: thesis:

end;

L is Subgroup of G9 by A29, Def7;
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:162;
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 Lm5; :: thesis:
A54: Ker ((nat_hom H99) * f99) = N1 by A52, A53, Lm5, Th88;

now

set f2 = (nat_hom H99) * f9;
let N19 be strict normal StableSubgroup of G9 "\/" N; :: thesis:
let N29 be strict normal StableSubgroup of G9; :: thesis:
assume A55: N19 = L "\/" N ; :: thesis:
( 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:159, RELAT_1:162;
then A56: ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = ((nat_hom H99) * f9) .: the carrier of G9 by RELAT_1:159;
A57: f9 " the carrier of (Ker (nat_hom H99)) = f9 " the carrier of H99 by Th48;
assume N29 = L "\/" (G9 /\ N) ; :: thesis:
then A58: N29 = Ker ((nat_hom H99) * f9) by A37, A41, A57, Lm5, Th88;
the carrier of (Image ((nat_hom H99) * f99)) = ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) by Def25
.= the carrier of (Image ((nat_hom H99) * f9)) by A56, Def25 ;
then A59: Image ((nat_hom H99) * f99) = Image ((nat_hom H99) * f9) by Lm5;
( (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:

end;

hence 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 ; :: thesis: