Cartesian Product Distributes over Set Difference

Theorem

$(1): \quad S \times \paren {T_1 \setminus T_2} = \paren {S \times T_1} \setminus \paren {S \times T_2}$
$(2): \quad \paren {T_1 \setminus T_2} \times S = \paren {T_1 \times S} \setminus \paren {T_2 \times S}$

Proof

 $\displaystyle$  $\displaystyle \tuple {x, y} \in S \times \paren {T_1 \setminus T_2}$ $\displaystyle$ $\leadstoandfrom$ $\displaystyle \paren {x \in S} \land \paren {y \in \paren {T_1 \setminus T_2} }$ Definition of Cartesian Product $\displaystyle$ $\leadstoandfrom$ $\displaystyle \paren {x \in S} \land \paren {y \in T_1} \land \paren {y \notin T_2}$ Definition of Set Difference $\displaystyle$ $\leadstoandfrom$ $\displaystyle \paren {\tuple {x, y} \in S \times T_1} \land \paren {\tuple {x, y} \notin S \times T_2}$ Definition of Cartesian Product $\displaystyle$ $\leadstoandfrom$ $\displaystyle \tuple {x, y} \in \paren {S \times T_1} \setminus \paren {S \times T_2}$ Definition of Set Difference

 $\displaystyle$  $\displaystyle \tuple {x, y} \in \paren {T_1 \setminus T_2} \times S$ $\displaystyle$ $\leadstoandfrom$ $\displaystyle \paren {x \in \paren {T_1 \setminus T_2} } \land \paren {y \in S}$ Definition of Cartesian Product $\displaystyle$ $\leadstoandfrom$ $\displaystyle \paren {x \in T_1} \land \paren {x \notin T_2} \land \paren {y \in S}$ Definition of Set Difference $\displaystyle$ $\leadstoandfrom$ $\displaystyle \paren {\tuple {x, y} \in T_1 \times S} \land \paren {\tuple {x, y} \notin T_2 \times S}$ Definition of Cartesian Product $\displaystyle$ $\leadstoandfrom$ $\displaystyle \tuple {x, y} \in \paren {T_1 \times S} \setminus \paren {T_2 \times S}$ Definition of Set Difference

$\blacksquare$