let O be set ; :: thesis:
let G, H be strict GroupWithOperators of O; :: thesis:
let N, L, G' be strict StableSubgroup of G; :: thesis:
reconsider N' = G' /\ N as StableSubgroup of G' by Lm34;
reconsider Gs' = multMagma(# the carrier of G',the multF of G' #) as strict Subgroup of G by Lm16;
let f be Homomorphism of G,H; :: thesis:
reconsider L'' = L as Subgroup of G by Def7;
assume A1: N = Ker f ; :: thesis:
then consider H' being strict StableSubgroup of H such that
A2: the carrier of H' = f .: the carrier of G' and
A3: f " the carrier of H' = the carrier of (G' "\/" N) and
( f is onto & G' is normal implies H' is normal ) by Th79;
reconsider f'' = f | the carrier of (G' "\/" N) as Homomorphism of (G' "\/" N),H' by A3, Th89;
reconsider Ns = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by A1, Lm7;
(carr Gs') * Ns = Ns * (carr Gs') by GROUP_3:143;
then A4: G' * N = N * G' ;

A5: now

let y be set ; :: thesis:
assume y in f .: the carrier of G' ; :: thesis:
then consider x being set such that
A6: x in dom f and
A7: x in the carrier of G' and
A8: y = f . x by FUNCT_1:def 12;
reconsider x = x as Element of by A6;
consider x' being set such that
A9: x' = x * (1_ G) ;
A10: x' 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 . x' 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 x' in G' * N by A7, A9;
hence y in f .: (G' * 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 .: (G' * N) ; :: thesis:
then consider x being set such that
A13: x in dom f and
A14: x in G' * N and
A15: y = f . x by FUNCT_1:def 12;
reconsider x = x as Element of by A13;
consider g1, g2 being Element of such that
A16: x = g1 * g2 and
A17: g1 in carr G' 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 G' by A12, A17, FUNCT_1:def 12; :: thesis:

end;

then f .: the carrier of G' = f .: (G' * N) by A5, TARSKI:2;
then A20: ( f'' .: the carrier of (G' "\/" N) = f .: the carrier of (G' "\/" N) & the carrier of H' = f .: the carrier of (G' "\/" N) ) by A2, A4, Th30, RELAT_1:162;

A21: now

let x be set ; :: thesis:
assume x in f'' " (f .: the carrier of L) ; :: thesis:
then A22: x in the carrier of (G' "\/" 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 by A22, A23;
consider g3 being Element of 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 f' = f | the carrier of G' as Homomorphism of G',H' by A2, Th89;

A27: now

let x be set ; :: thesis:
assume x in the carrier of N' ; :: thesis:
then A28: x in (carr G') /\ (carr N) by Def28;
then reconsider a' = x as Element of by XBOOLE_0:def 4;
reconsider a'' = a' as Element of by Th2;
x in carr N by A28, XBOOLE_0:def 4;
then x in N by STRUCT_0:def 5;
then f . a'' = 1_ H by A1, Th47;
then f . a' = 1_ H' by Th4;
then f' . a' = 1_ H' by FUNCT_1:72;
hence x in { a where a is Element of : f' . a = 1_ H' } ; :: thesis:

end;

assume A29: L is strict normal StableSubgroup of G' ; :: thesis:
then reconsider L' = L as strict StableSubgroup of G' ;
reconsider N1 = L "\/" N as StableSubgroup of G' "\/" N by A29, Th38;
(carr L'') * Ns = Ns * (carr L'') 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 : f' . a = 1_ H' } ; :: thesis:
then consider a being Element of such that
A31: x = a and
A32: f' . a = 1_ H' ;
reconsider a = a as Element of by Th2;
f . a = 1_ H' 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 G') /\ (carr N) by A31, XBOOLE_0:def 4;
hence x in the carrier of N' by Def28; :: thesis:

end;

then the carrier of N' = { a where a is Element of : f' . a = 1_ H' } by A27, TARSKI:2;
then A33: N' = Ker f' by Def24;
then consider H'' being strict StableSubgroup of H' such that
A34: the carrier of H'' = f' .: the carrier of L' and
A35: f' " the carrier of H'' = the carrier of (L' "\/" N') and
A36: ( f' is onto & L' is normal implies H'' is normal ) by Th79;
consider N2 being strict StableSubgroup of G' such that
A37: the carrier of N2 = f' " the carrier of H'' and
A38: ( H'' is normal implies ( N' is normal StableSubgroup of N2 & N2 is normal ) ) by A33, Th78;
( f' .: the carrier of G' = f .: the carrier of G' & H' is strict StableSubgroup of H' ) by Lm4, RELAT_1:162;
then Image f' = H' by A2, Def25;
then A39: rng f' = the carrier of H' by Th49;
then reconsider H'' = H'' as normal StableSubgroup of H' by A29, A36, FUNCT_2:def 3;
A40: N2 = L' "\/" N' by A35, A37, Lm5;
hence L "\/" (G' /\ N) is normal StableSubgroup of G' by A29, A36, A38, A39, Th86, FUNCT_2:def 3; :: thesis:
set l = nat_hom H'';
set f1 = (nat_hom H'') * f'';
A41: N2 = L "\/" (G' /\ N) by A40, Th86;
A42: L "\/" N is StableSubgroup of G' "\/" 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 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 G' "\/" N by A42, Def7;
then A50: the carrier of (L "\/" N) c= the carrier of (G' "\/" N) by GROUP_2:def 5;
A51: x in the carrier of (L "\/" N) by A30, A44, Th30;
then x in G' "\/" 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 (G' "\/" N) /\ (f " (f .: the carrier of L)) by A51, A50, XBOOLE_0:def 4;
hence x in f'' " (f .: the carrier of L) by FUNCT_1:139; :: thesis:

end;

L is Subgroup of G' by A29, Def7;
then the carrier of L c= the carrier of G' by GROUP_2:def 5;
then f' .: the carrier of L = f .: the carrier of L by RELAT_1:162;
then f'' " (f' .: the carrier of L) = L * N by A21, A43, TARSKI:2;
then A52: f'' " the carrier of H'' = the carrier of N1 by A34, A30, Th30;
A53: f'' " the carrier of (Ker (nat_hom H'')) = f'' " the carrier of H'' by Th48;
then the carrier of (Ker ((nat_hom H'') * f'')) = the carrier of N1 by A52, Th88;
hence L "\/" N is normal StableSubgroup of G' "\/" N by Lm5; :: thesis:
A54: Ker ((nat_hom H'') * f'') = N1 by A52, A53, Lm5, Th88;

now

set f2 = (nat_hom H'') * f';
let N1' be strict normal StableSubgroup of G' "\/" N; :: thesis:
let N2' be strict normal StableSubgroup of G'; :: thesis:
assume A55: N1' = L "\/" N ; :: thesis:
( f'' .: the carrier of (G' "\/" N) = f' .: the carrier of G' & ((nat_hom H'') * f'') .: the carrier of (G' "\/" N) = (nat_hom H'') .: (f'' .: the carrier of (G' "\/" N)) ) by A2, A20, RELAT_1:159, RELAT_1:162;
then A56: ((nat_hom H'') * f'') .: the carrier of (G' "\/" N) = ((nat_hom H'') * f') .: the carrier of G' by RELAT_1:159;
A57: f' " the carrier of (Ker (nat_hom H'')) = f' " the carrier of H'' by Th48;
assume N2' = L "\/" (G' /\ N) ; :: thesis:
then A58: N2' = Ker ((nat_hom H'') * f') by A37, A41, A57, Lm5, Th88;
the carrier of (Image ((nat_hom H'') * f'')) = ((nat_hom H'') * f'') .: the carrier of (G' "\/" N) by Def25
.= the carrier of (Image ((nat_hom H'') * f')) by A56, Def25 ;
then A59: Image ((nat_hom H'') * f'') = Image ((nat_hom H'') * f') by Lm5;
( (G' "\/" N) ./. (Ker ((nat_hom H'') * f'')), Image ((nat_hom H'') * f'') are_isomorphic & Image ((nat_hom H'') * f'),G' ./. (Ker ((nat_hom H'') * f')) are_isomorphic ) by Th59;
hence (G' "\/" N) ./. N1',G' ./. N2' are_isomorphic by A54, A55, A59, A58, Th55; :: thesis:

end;

hence for N1 being strict normal StableSubgroup of G' "\/" N
for N2 being strict normal StableSubgroup of G' st N1 = L "\/" N & N2 = L "\/" (G' /\ N) holds
(G' "\/" N) ./. N1,G' ./. N2 are_isomorphic ; :: thesis: