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 & (N1 ` H) * (N2 ` H) c= N ` H )
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 & (N1 ` H) * (N2 ` H) c= N ` H )
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 & (N1 ` H) * (N2 ` H) c= N ` H )
consider N being strict normal Subgroup of G such that
A1: the carrier of N = N1 * N2 by Th8;
(N1 ` H) * (N2 ` H) c= N ` H

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N1 ` H) * (N2 ` H) or x in N ` H )
assume A2: x in (N1 ` H) * (N2 ` H) ; :: thesis: x in N ` H
then reconsider x = x as Element of G ;
consider a, b being Element of G such that
A3: ( x = a * b & a in N1 ` H & b in N2 ` H ) by A2;
( a * N1 c= carr H & b * N2 c= carr H ) by A3, Th49;
then (a * N1) * (b * N2) c= (carr H) * (carr H) by GROUP_3:4;
then A4: (a * N1) * (b * N2) c= carr H by GROUP_2:76;
(a * N1) * (b * N2) = (a * b) * N by A1, Th10;
hence x in N ` H by A3, A4; :: thesis: verum

end;

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