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 ` 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 & N ` H c= (N1 ` H) /\ (N2 ` 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 & N ` H c= (N1 ` H) /\ (N2 ` H) )

consider N being strict normal Subgroup of G such that

A1: the carrier of N = N1 * N2 by Th8;

( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9;

then A2: ( N ` H c= N1 ` H & N ` H c= N2 ` H ) by Th60;

N ` H c= (N1 ` H) /\ (N2 ` H) by A2, XBOOLE_0:def 4;

hence ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) by A1; :: thesis: verum

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 ` 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 & N ` H c= (N1 ` H) /\ (N2 ` 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 & N ` H c= (N1 ` H) /\ (N2 ` H) )

consider N being strict normal Subgroup of G such that

A1: the carrier of N = N1 * N2 by Th8;

( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9;

then A2: ( N ` H c= N1 ` H & N ` H c= N2 ` H ) by Th60;

N ` H c= (N1 ` H) /\ (N2 ` H) by A2, XBOOLE_0:def 4;

hence ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) by A1; :: thesis: verum