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

( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` 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 & (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

hence
ex N being strict normal Subgroup of G st
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;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

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