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

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