Theorem: External Direct Product of Congruence Relations

Let $\struct {A, \odot}$ and $\struct {B, \circledast}$ be algebraic structures.
Let $\RR$ and $\SS$ be congruence relations on $\struct {A, \odot}$ and $\struct {B, \circledast}$ respectively.
Let $\struct {A / \RR, \odot_\RR}$ and $\struct {B / \SS, \circledast_\SS}$ denote the quotient structures defined by $\RR$ and $\SS$ respectively.
Let $\struct {A \times B, \otimes}$ be the external direct product of $\struct {A, \odot}$ and $\struct {B, \circledast}$.
Let $\TT$ be the relation on $\struct {A \times B, \otimes}$ defined as:
:$\forall \tuple {u, v}, \tuple {x, y} \in A \times B: \tuple {u, v} \mathrel \TT \tuple {x, y} \iff u \mathrel \RR x \land v \mathrel \SS y$
Then:
:$\TT$ is a congruence relation on $\struct {A \times B, \otimes}$
and the mapping $h: \struct {A / \RR, \odot_\RR} \times \struct {B / \SS, \circledast_\SS} \to \struct {\paren {A \times B} / \TT, \otimes_\TT}$ defined as:
:$\forall \tuple {\eqclass x \RR, \eqclass y \SS} \in \struct {A / \RR, \odot_\RR} \times \struct {B / \SS, \circledast_\SS}: \map h {\eqclass x \RR, \eqclass y \SS} = \eqclass {\tuple {x, y} } \TT$
is an isomorphism.

Proof:
We have that $\RR$ and $\SS$ are congruence relations on $\struct {A, \odot}$ and $\struct {B, \circledast}$ respectively.
Hence {{afortiori}} $\RR$ and $\SS$ are equivalence relations on $A$ and $B$ respectively.
Thus from Cartesian Product of Equivalence Relations we have that $\TT$ is an equivalence relation.
Let $\tuple {a_1, b_1}, \tuple {a_2, b_2}, \tuple {c_1, d_1}, \tuple {c_2, d_2} \in A \times B$ be such that:
{{begin-eqn}}
{{eqn | l = \tuple {a_1, b_1}
      | o = \TT
      | r = \tuple {a_2, b_2}
}}
{{eqn | l = \tuple {c_1, d_1}
      | o = \TT
      | r = \tuple {c_2, d_2}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a_1
      | o = \RR
      | r = a_2
      | c = Definition of $\TT$
}}
{{eqn | lo= \land
      | l = c_1
      | o = \RR
      | r = c_2
      | c = 
}}
{{eqn | lo= \land
      | l = b_1
      | o = \SS
      | r = b_2
      | c = 
}}
{{eqn | lo= \land
      | l = d_1
      | o = \SS
      | r = d_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a_1 \odot c_1
      | o = \RR
      | r = a_2 \odot c_2
      | c = {{Defof|Congruence Relation}}
}}
{{eqn | lo= \land
      | l = b_1 \circledast d_1
      | o = \SS
      | r = b_2 \circledast d_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {a_1 \odot c_1, b_1 \circledast d_1}
      | o = \TT
      | r = \tuple {a_2 \odot c_2, b_2 \circledast d_2}
      | c = Definition of $\TT$
}}
{{eqn | ll= \leadsto
      | l = \tuple {a_1, b_1} \otimes \tuple {c_1, d_1}
      | o = \TT
      | r = \tuple {a_2, b_2} \otimes \tuple {c_2, d_2}
      | c = {{Defof|External Direct Product}}
}}
{{end-eqn}}
Hence by definition $\TT$ is a congruence relation on $\struct {A \times B, \otimes}$.
It remains to be shown that $h$ as defined is an isomorphism.
From Cartesian Product of Equivalence Relations, the equivalence class of $\tuple {a, b} \in A \times B$ is:
:$\eqclass {\tuple {a, b} } \TT = \set {\tuple {x, y}: x \in \eqclass a \RR, y \in \eqclass b \SS}$
{{finish|intuitively obvious, tedious proving it rigorously}}