let G be Group; :: thesis: for H being Subgroup of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) )
let H be Subgroup of G; :: thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) )
let N1, N2 be strict normal Subgroup of G; :: thesis: ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) )
consider N being strict normal Subgroup of G such that
A1: the carrier of N = N1 * N2 by Th8;
N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ H or x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) )
assume A2: x in N ~ H ; :: thesis: x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1)
then reconsider x = x as Element of G ;
x * N meets carr H by A2, Th51;
then consider x1 being set such that
A4: ( x1 in x * N & x1 in carr H ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of G by A4;
consider y being Element of G such that
A5: ( x1 = x * y & y in N ) by A4, GROUP_2:125;
A6: y in N1 * N2 by A1, A5, STRUCT_0:def 5;
then consider a, b being Element of G such that
A7: ( y = a * b & a in N1 & b in N2 ) by Th6;
A8: x1 = (x * a) * b by A5, A7, GROUP_1:def 4;
a in carr N1 by A7, STRUCT_0:def 5;
then A9: (x * a) * b in (x * N1) * b by GROUP_8:15;
(x * N1) * b = x * (N1 * b) by GROUP_2:128
.= x * (b * N1) by GROUP_3:140
.= (x * b) * N1 by GROUP_2:127 ;
then (x * b) * N1 meets carr H by A4, A8, A9, XBOOLE_0:3;
then A10: x * b in N1 ~ H ;
A11: (x * b) * (b " ) = x * (b * (b " )) by GROUP_1:def 4
.= x * (1_ G) by GROUP_1:def 6
.= x by GROUP_1:def 5 ;
b " in N2 by A7, GROUP_2:60;
then A12: x in (N1 ~ H) * N2 by A10, A11, GROUP_2:114;
y in N2 * N1 by A6, GROUP_3:148;
then consider a, b being Element of G such that
A13: ( y = a * b & a in N2 & b in N1 ) by Th6;
A14: x1 = (x * a) * b by A5, A13, GROUP_1:def 4;
a in carr N2 by A13, STRUCT_0:def 5;
then A15: (x * a) * b in (x * N2) * b by GROUP_8:15;
(x * N2) * b = x * (N2 * b) by GROUP_2:128
.= x * (b * N2) by GROUP_3:140
.= (x * b) * N2 by GROUP_2:127 ;
then (x * b) * N2 meets carr H by A4, A14, A15, XBOOLE_0:3;
then A16: x * b in N2 ~ H ;
A17: (x * b) * (b " ) = x * (b * (b " )) by GROUP_1:def 4
.= x * (1_ G) by GROUP_1:def 6
.= x by GROUP_1:def 5 ;
b " in N1 by A13, GROUP_2:60;
then x in (N2 ~ H) * N1 by A16, A17, GROUP_2:114;
hence x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) by A12, XBOOLE_0:def 4; :: thesis: verum

end;

hence ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) by A1; :: thesis: verum