let G be Group; :: thesis: for A, B being non empty Subset of G
for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B)
let A, B be non empty Subset of G; :: thesis: for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B)
let N be normal Subgroup of G; :: thesis: (N ` A) * (N ` B) c= N ` (A * B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (N ` A) * (N ` B) or x in N ` (A * B) )
assume A1: x in (N ` A) * (N ` B) ; :: thesis: x in N ` (A * B)
then reconsider x = x as Element of G ;
consider x1, x2 being Element of G such that
A2: ( x = x1 * x2 & x1 in N ` A & x2 in N ` B ) by A1;
( x1 * N c= A & x2 * N c= B ) by A2, Th12;
then (x1 * N) * (x2 * N) c= A * B by GROUP_3:4;
then (x1 * x2) * N c= A * B by Th1;
hence x in N ` (A * B) by A2; :: thesis: verum