let G be strict Group; :: thesis: for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let H, F2 be strict Subgroup of G; :: thesis: for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let F1 be strict normal Subgroup of F2; :: thesis: for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
reconsider G2 = H /\ F2 as strict Subgroup of G ;
consider f being Function such that
A1: f = (nat_hom F1) | the carrier of H ;
reconsider f1 = nat_hom F1 as Function of the carrier of F2, the carrier of (F2 ./. F1) ;
A2: ( the carrier of F2 = carr F2 & the carrier of H = carr H ) ;
dom f1 = the carrier of F2 by FUNCT_2:def 1;
then A3: dom f = the carrier of F2 /\ the carrier of H by A1, RELAT_1:90
.= carr (F2 /\ H) by A2, GROUP_2:98
.= the carrier of (H /\ F2) ;
rng ((nat_hom F1) | the carrier of H) c= rng (nat_hom F1) by RELAT_1:99;
then reconsider f = f as Function of the carrier of (H /\ F2), the carrier of (F2 ./. F1) by A1, A3, FUNCT_2:4;
for a, b being Element of (H /\ F2) holds f . (a * b) = (f . a) * (f . b)

proof

let a, b be Element of (H /\ F2); :: thesis: f . (a * b) = (f . a) * (f . b)
A4: the carrier of (H /\ F2) = (carr H) /\ (carr F2) by GROUP_2:def 10;
then reconsider a9 = a, b9 = b as Element of F2 by XBOOLE_0:def 4;
b in carr H by A4, XBOOLE_0:def 4;
then A5: ((nat_hom F1) | the carrier of H) . b = (nat_hom F1) . b by FUNCT_1:72;
a * b in carr H by A4, XBOOLE_0:def 4;
then A6: ((nat_hom F1) | the carrier of H) . (a * b) = (nat_hom F1) . (a * b) by FUNCT_1:72;
H /\ F2 is Subgroup of F2 by GROUP_2:106;
then A7: a * b = a9 * b9 by GROUP_2:52;
a in carr H by A4, XBOOLE_0:def 4;
then ((nat_hom F1) | the carrier of H) . a = (nat_hom F1) . a by FUNCT_1:72;
hence f . (a * b) = (f . a) * (f . b) by A1, A7, A5, A6, GROUP_6:def 7; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (H /\ F2),(F2 ./. F1) by GROUP_6:def 7;
A8: the carrier of H /\ the carrier of F2 = carr (H /\ F2) by A2, GROUP_2:98
.= the carrier of (H /\ F2) ;
A9: Ker f = H /\ F1

proof

reconsider L = Ker f as Subgroup of G by GROUP_2:65;
for g being Element of G holds
( g in L iff g in H /\ F1 )

proof

let x be Element of G; :: thesis: ( x in L iff x in H /\ F1 )
thus ( x in L implies x in H /\ F1 ) :: thesis: ( x in H /\ F1 implies x in L )

proof

assume A10: x in L ; :: thesis: x in H /\ F1
then x in carr (Ker f) by STRUCT_0:def 5;
then reconsider a = x as Element of (H /\ F2) ;
A11: the carrier of (H /\ F2) = (carr H) /\ (carr F2) by GROUP_2:def 10;
then reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;
A12: a in carr H by A11, XBOOLE_0:def 4;
then A13: a in H by STRUCT_0:def 5;
((nat_hom F1) | the carrier of H) . a = (nat_hom F1) . a by A12, FUNCT_1:72;
then A14: f . a = a9 * F1 by A1, GROUP_6:def 9;
f . a = 1_ (F2 ./. F1) by A10, GROUP_6:50
.= carr F1 by GROUP_6:29 ;
then a9 in F1 by A14, GROUP_2:136;
hence x in H /\ F1 by A13, GROUP_2:99; :: thesis: verum

end;

thus ( x in H /\ F1 implies x in L ) :: thesis: verum

proof

reconsider F19 = F1 as strict Subgroup of G ;
A15: the carrier of H /\ the carrier of F1 = (carr H) /\ (carr F19)
.= the carrier of (H /\ F1) by GROUP_2:def 10 ;
assume x in H /\ F1 ; :: thesis: x in L
then A16: x in carr (H /\ F1) by STRUCT_0:def 5;
the carrier of F1 c= the carrier of F2 by GROUP_2:def 5;
then the carrier of (H /\ F1) c= the carrier of (H /\ F2) by A8, A15, XBOOLE_1:26;
then reconsider a = x as Element of (H /\ F2) by A16;
x in the carrier of F1 by A16, A15, XBOOLE_0:def 4;
then A17: a in F1 by STRUCT_0:def 5;
A18: the carrier of (H /\ F2) = (carr H) /\ (carr F2) by GROUP_2:def 10;
then reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;
a in carr H by A18, XBOOLE_0:def 4;
then ((nat_hom F1) | the carrier of H) . a = (nat_hom F1) . a by FUNCT_1:72;
then f . a = a9 * F1 by A1, GROUP_6:def 9
.= carr F1 by A17, GROUP_2:136
.= 1_ (F2 ./. F1) by GROUP_6:29 ;
hence x in L by GROUP_6:50; :: thesis: verum

end;

end;

hence Ker f = H /\ F1 by GROUP_2:def 6; :: thesis: verum

end;

reconsider G1 = Ker f as strict normal Subgroup of G2 ;
G2 ./. G1, Image f are_isomorphic by GROUP_6:90;
hence for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic by A9; :: thesis: verum