Prove that a function is bijective Let $A_1,A_2,B$  be sets, the function $\varphi:A_1 \to A_2$  is a bijection. I need to build a bijection $F: A_1 \times B \to A_2 \times B.$
It is clear  that the function $F$ defined  by $F(a_1,b)=(\varphi(a_1),b), a_1 \in A_1$ is such a bijection. But  how  to prove it accurately?  For any $(a_2,b) \in A_2 \times B$ I can find the inverse $F^{-1}$  by $F^{-1}(a_2,b)=(\varphi^{-1}(a_2), b)$.  Is that  enough   to prove  that $F$ is bijective?
 A: (1). $F: A_1 \times B \rightarrow A_2 \times B, (a, b) \mapsto (\phi(a), b).$
$F$ is injective: Let $(x_1, y_1), (x_2, y_2) \in A_1 \times B$ be such that $F(x_1, y_1) = F(x_2, y_2).$ Then $(\phi(x_1), y_1) = (\phi(x_2), y_2) \Rightarrow y_1 = y_2, \phi(x_1) = \phi(x_2) \Rightarrow y_1 = y_2, x_1 = x_2$.
$F$ is surjective: Let $(x, y) \in A_2 \times B.$ Then there exists $a \in A_1, \phi(a) = x.$ So $F(a, y) = (x, y).$
(2). $\phi: A_1 \rightarrow A_2$ is a bijection. Let $\psi := \phi^{-1}.$ Then $\psi: A_2 \rightarrow A_1$ is a bijection. Also $\phi \psi : A_2 \rightarrow A_2$ is the identity map and $\psi \phi: A_1 \rightarrow A_1$ is the identity map.
Define $G : A_2 \times B \rightarrow A_1 \times B$ by $(a, b) \mapsto (\psi(a), b).$ Now $FG : A_2\times B \rightarrow A_2 \times B$ is a map satisfying $FG(a,b) = F(G(a, b)) = F(\psi(a), b) = F(\phi\psi(a), b) = (a, b).$ Also $GF : A_1 \times B \rightarrow A_1 \times B$ is a map satisfying $GF(a, b) = G(F(a, b)) = G(\phi(a), b) = (\psi\phi(a), b) = (a, b).$ Thus $FG$ and $GF$ are identity maps on $A_2 \times B$ and $A_1 \times B$ respectively. Hence $F$ is bijective.
