let G be Group; :: thesis: for H1, H2 being Subgroup of G

for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)

let H1, H2 be Subgroup of G; :: thesis: for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)

let N be normal Subgroup of G; :: thesis: (N ` H1) * (N ` H2) c= N ` (H1 * H2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ` H1) * (N ` H2) or x in N ` (H1 * H2) )

assume A1: x in (N ` H1) * (N ` H2) ; :: thesis: x in N ` (H1 * H2)

then reconsider x = x as Element of G ;

consider x1, x2 being Element of G such that

A2: ( x = x1 * x2 & x1 in N ` H1 & x2 in N ` H2 ) by A1;

( x1 * N c= carr H1 & x2 * N c= carr H2 ) by A2, Th49;

then (x1 * N) * (x2 * N) c= (carr H1) * (carr H2) by GROUP_3:4;

then (x1 * x2) * N c= (carr H1) * (carr H2) by Th1;

hence x in N ` (H1 * H2) by A2; :: thesis: verum

for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)

let H1, H2 be Subgroup of G; :: thesis: for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)

let N be normal Subgroup of G; :: thesis: (N ` H1) * (N ` H2) c= N ` (H1 * H2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ` H1) * (N ` H2) or x in N ` (H1 * H2) )

assume A1: x in (N ` H1) * (N ` H2) ; :: thesis: x in N ` (H1 * H2)

then reconsider x = x as Element of G ;

consider x1, x2 being Element of G such that

A2: ( x = x1 * x2 & x1 in N ` H1 & x2 in N ` H2 ) by A1;

( x1 * N c= carr H1 & x2 * N c= carr H2 ) by A2, Th49;

then (x1 * N) * (x2 * N) c= (carr H1) * (carr H2) by GROUP_3:4;

then (x1 * x2) * N c= (carr H1) * (carr H2) by Th1;

hence x in N ` (H1 * H2) by A2; :: thesis: verum