let G be Group; :: thesis: for H1, H2 being Subgroup of G
for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)
let H1, H2 be Subgroup of G; :: thesis: for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)
let N be normal Subgroup of G; :: thesis: (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)
thus (N ~ H1) * (N ~ H2) c= N ~ (H1 * H2) :: according to XBOOLE_0:def 10 :: thesis: N ~ (H1 * H2) c= (N ~ H1) * (N ~ H2)

proof

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;
A3: x1 * N meets carr H1 by A2, Th51;
A4: x2 * N meets carr H2 by A2, Th51;
consider x19 being object such that
A5: ( x19 in x1 * N & x19 in carr H1 ) by A3, XBOOLE_0:3;
consider x29 being object such that
A6: ( x29 in x2 * N & x29 in carr H2 ) 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 (carr H1) * (carr H2) by A5, A6;
x19 * x29 in (x1 * N) * (x2 * N) by A5, A6;
then (x1 * N) * (x2 * N) meets (carr H1) * (carr H2) by A7, XBOOLE_0:3;
then (x1 * x2) * N meets (carr H1) * (carr H2) by Th1;
hence x in N ~ (H1 * H2) by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ (H1 * H2) or x in (N ~ H1) * (N ~ H2) )
assume A8: x in N ~ (H1 * H2) ; :: thesis: x in (N ~ H1) * (N ~ H2)
then reconsider x = x as Element of G ;
x * N meets (carr H1) * (carr H2) by A8, Th28;
then consider x1 being object such that
A9: ( x1 in x * N & x1 in (carr H1) * (carr H2) ) 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 carr H1 & y2 in carr H2 ) 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 carr H1 & g2 * N meets carr H2 ) by A10, XBOOLE_0:3;
then ( g1 in N ~ H1 & g2 in N ~ H2 ) ;
hence x in (N ~ H1) * (N ~ H2) by A11; :: thesis: verum