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 ;
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 ;
A5: y in N1 * N2 by ;
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 ;
a in carr N1 by ;
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 ;
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 ;
then A11: x in (N1 ~ H) * N2 by ;
y in N2 * N1 by ;
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 ;
a in carr N2 by ;
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 ;
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 ;
then x in (N2 ~ H) * N1 by ;
hence x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) by ; :: 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