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) = 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) = 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)

assume A8: x in N ~ (A * B) ; :: thesis: x in (N ~ A) * (N ~ B)

then reconsider x = x as Element of G ;

x * N meets A * B by A8, Th28;

then consider x1 being object such that

A9: ( x1 in x * N & x1 in A * B ) by XBOOLE_0:3;

reconsider x1 = x1 as Element of G by A9;

consider y1, y2 being Element of G such that

A10: ( x1 = y1 * y2 & y1 in A & y2 in B ) by A9;

x * N = (y1 * y2) * N by A9, A10, Th2

.= (y1 * N) * (y2 * N) by Th1 ;

then x in (y1 * N) * (y2 * N) by GROUP_2:108;

then consider g1, g2 being Element of G such that

A11: ( x = g1 * g2 & g1 in y1 * N & g2 in y2 * N ) ;

( y1 * N = g1 * N & y2 * N = g2 * N ) by A11, Th2;

then ( y1 in g1 * N & y2 in g2 * N ) by GROUP_2:108;

then ( g1 * N meets A & g2 * N meets B ) by A10, XBOOLE_0:3;

then ( g1 in N ~ A & g2 in N ~ B ) ;

hence x in (N ~ A) * (N ~ B) by A11; :: thesis: verum

for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = 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) = 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (A * B) or x in (N ~ A) * (N ~ 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;

A3: x1 * N meets A by A2, Th14;

A4: x2 * N meets B by A2, Th14;

consider x19 being object such that

A5: ( x19 in x1 * N & x19 in A ) by A3, XBOOLE_0:3;

consider x29 being object such that

A6: ( x29 in x2 * N & x29 in B ) by A4, XBOOLE_0:3;

reconsider x19 = x19 as Element of G by A5;

reconsider x29 = x29 as Element of G by A6;

A7: x19 * x29 in A * B by A5, A6;

x19 * x29 in (x1 * N) * (x2 * N) by A5, A6;

then (x1 * N) * (x2 * N) meets A * B by A7, XBOOLE_0:3;

then (x1 * x2) * N meets A * B by Th1;

hence x in N ~ (A * B) by A2; :: thesis: verum

end;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;

A3: x1 * N meets A by A2, Th14;

A4: x2 * N meets B by A2, Th14;

consider x19 being object such that

A5: ( x19 in x1 * N & x19 in A ) by A3, XBOOLE_0:3;

consider x29 being object such that

A6: ( x29 in x2 * N & x29 in B ) by A4, XBOOLE_0:3;

reconsider x19 = x19 as Element of G by A5;

reconsider x29 = x29 as Element of G by A6;

A7: x19 * x29 in A * B by A5, A6;

x19 * x29 in (x1 * N) * (x2 * N) by A5, A6;

then (x1 * N) * (x2 * N) meets A * B by A7, XBOOLE_0:3;

then (x1 * x2) * N meets A * B by Th1;

hence x in N ~ (A * B) by A2; :: thesis: verum

assume A8: x in N ~ (A * B) ; :: thesis: x in (N ~ A) * (N ~ B)

then reconsider x = x as Element of G ;

x * N meets A * B by A8, Th28;

then consider x1 being object such that

A9: ( x1 in x * N & x1 in A * B ) by XBOOLE_0:3;

reconsider x1 = x1 as Element of G by A9;

consider y1, y2 being Element of G such that

A10: ( x1 = y1 * y2 & y1 in A & y2 in B ) by A9;

x * N = (y1 * y2) * N by A9, A10, Th2

.= (y1 * N) * (y2 * N) by Th1 ;

then x in (y1 * N) * (y2 * N) by GROUP_2:108;

then consider g1, g2 being Element of G such that

A11: ( x = g1 * g2 & g1 in y1 * N & g2 in y2 * N ) ;

( y1 * N = g1 * N & y2 * N = g2 * N ) by A11, Th2;

then ( y1 in g1 * N & y2 in g2 * N ) by GROUP_2:108;

then ( g1 * N meets A & g2 * N meets B ) by A10, XBOOLE_0:3;

then ( g1 in N ~ A & g2 in N ~ B ) ;

hence x in (N ~ A) * (N ~ B) by A11; :: thesis: verum