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 object ; :: 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 object such that
A3: ( x1 in x * N & x1 in carr H ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of G by A3;
consider y being Element of G such that
A4: ( x1 = x * y & y in N ) by A3, GROUP_2:103;
A5: y in N1 * N2 by A1, A4, STRUCT_0:def 5;
then consider a, b being Element of G such that
A6: ( y = a * b & a in N1 & b in N2 ) by Th6;
A7: x1 = (x * a) * b by A4, A6, GROUP_1:def 3;
a in carr N1 by A6, STRUCT_0:def 5;
then A8: (x * a) * b in (x * N1) * b by GROUP_8:15;
(x * N1) * b = x * (N1 * b) by GROUP_2:106
.= x * (b * N1) by GROUP_3:117
.= (x * b) * N1 by GROUP_2:105 ;
then (x * b) * N1 meets carr H by A3, A7, A8, XBOOLE_0:3;
then A9: x * b in N1 ~ H ;
A10: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def 3
.= x * (1_ G) by GROUP_1:def 5
.= x by GROUP_1:def 4 ;
b " in N2 by A6, GROUP_2:51;
then A11: x in (N1 ~ H) * N2 by A9, A10, GROUP_2:94;
y in N2 * N1 by A5, GROUP_3:125;
then consider a, b being Element of G such that
A12: ( y = a * b & a in N2 & b in N1 ) by Th6;
A13: x1 = (x * a) * b by A4, A12, GROUP_1:def 3;
a in carr N2 by A12, STRUCT_0:def 5;
then A14: (x * a) * b in (x * N2) * b by GROUP_8:15;
(x * N2) * b = x * (N2 * b) by GROUP_2:106
.= x * (b * N2) by GROUP_3:117
.= (x * b) * N2 by GROUP_2:105 ;
then (x * b) * N2 meets carr H by A3, A13, A14, XBOOLE_0:3;
then A15: x * b in N2 ~ H ;
A16: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def 3
.= x * (1_ G) by GROUP_1:def 5
.= x by GROUP_1:def 4 ;
b " in N1 by A12, GROUP_2:51;
then x in (N2 ~ H) * N1 by A15, A16, GROUP_2:94;
hence x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) by A11, 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