let G be Group; :: thesis: for A, B being non empty Subset of
for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)
let A, B be non empty Subset of ; :: thesis: for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)
let N be normal Subgroup of G; :: thesis: (N ~ A) * (N ~ B) = N ~ (A * B)
thus (N ~ A) * (N ~ B) c= N ~ (A * B) :: according to XBOOLE_0:def 10 :: thesis: N ~ (A * B) c= (N ~ A) * (N ~ B)

proof

let x be set ; :: 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 ;
consider x1, x2 being Element of such that
A2: ( x = x1 * x2 & x1 in N ~ A & x2 in N ~ B ) by A1;
A3: x1 * N meets A by A2, Th14;
A4: x2 * N meets B by A2, Th14;
consider x1' being set such that
A5: ( x1' in x1 * N & x1' in A ) by A3, XBOOLE_0:3;
consider x2' being set such that
A6: ( x2' in x2 * N & x2' in B ) by A4, XBOOLE_0:3;
reconsider x1' = x1' as Element of by A5;
reconsider x2' = x2' as Element of by A6;
A7: x1' * x2' in A * B by A5, A6;
A8: x1' * x2' in (x1 * N) * (x2 * N) by A5, A6;
(x1 * N) * (x2 * N) meets A * B by A7, A8, XBOOLE_0:3;
then (x1 * x2) * N meets A * B by Th1;
hence x in N ~ (A * B) by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (A * B) or x in (N ~ A) * (N ~ B) )
assume A9: x in N ~ (A * B) ; :: thesis: x in (N ~ A) * (N ~ B)
then reconsider x = x as Element of ;
A10: x * N meets A * B by A9, Th28;
consider x1 being set such that
A11: ( x1 in x * N & x1 in A * B ) by A10, XBOOLE_0:3;
reconsider x1 = x1 as Element of by A11;
consider y1, y2 being Element of such that
A12: ( x1 = y1 * y2 & y1 in A & y2 in B ) by A11;
A13: x * N = (y1 * y2) * N by A11, A12, Th2
.= (y1 * N) * (y2 * N) by Th1 ;
x in (y1 * N) * (y2 * N) by GROUP_2:130, A13;
then consider g1, g2 being Element of such that
A14: ( x = g1 * g2 & g1 in y1 * N & g2 in y2 * N ) ;
( y1 * N = g1 * N & y2 * N = g2 * N ) by A14, Th2;
then ( y1 in g1 * N & y2 in g2 * N ) by GROUP_2:130;
then ( g1 * N meets A & g2 * N meets B ) by A12, XBOOLE_0:3;
then ( g1 in N ~ A & g2 in N ~ B ) ;
hence x in (N ~ A) * (N ~ B) by A14; :: thesis: verum