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