Cartesian product of finite sets - check my proof 
Let $A$ und $B$ be non-empty finite sets. Then the Cartesian product is finite and it holds $$ \vert A \times B\vert = \vert A \vert \cdot \vert B \vert .$$

My proof:
As $A$ und $B$ are finite we have two bijections $f: A \to [m]$ and $g:B\to [n]$, where $[m], [n]$ are the intervalls $[1, ..., m]$ and $[1, ..., n]$ in $\mathbb{N}$, respectively. I define the following function $h: A\times B \to [m\cdot n]$,
$$h(a,b) = f(a)+(g(b)-1)m$$
The function $h$ is injective because it's simply a composition of injective functions (note that $m>0$). Let $y \in [m\cdot n]$ then there exists a $k \in [n]$ such that $(k-1)m < y \leq km$. Also, $y-(k-1)m \in [m]$. So there exist two elements $a \in A $ with $f(a) = y-(k-1)m$ and $b \in B$ with $g(b) = k$. Pluggin them into $h$ yields: $h(a,b) = f(a)+(g(b)-1)m=y-(k-1)m+m(k-1)=y$. As $y$ was arbitrarily chosen, every element of $[m\cdot n]$ has a preimage. Hence, $h$ is bijective so that $A \times B$ is finite and has a cardinality of $\vert A \times B\vert =mn=\vert A \vert \cdot \vert B \vert$.
Is this correct?
Or would you do it differently?
 A: I wouldn't do it any differently but I would probably only put in half the effort you did.  
Although it's important to realize that "Assume $A$ has $n$ elements" is, when you first walk into a class informal and poorly defined and not acceptable, and that the concept that saying something is finite means "there exists a bijection $f:A \to \mathbb N_n = \{1,....., n\}$" is a formal and precise definition, and that we have to use it to prove the must trivial and basic concepts of counting which we used to take for granted,... all that is true.  BUT that doesn't mean that once we have proven and defined those that we can't go back to using intuitive terms like "Assume $A$ has $n$ elements".  We can... now that we know that "$A$ has $n$ elements" means there is a bijection between $A$ and $\{1,....,n\}$.
That point is:
$|A| = n \iff $ there exists a bijection $f:A \to \{1,....,n\}\iff $ we can write $A$ as $A = \{a_1, ...., a_n\}\iff $ "let $a_k = f(k)$" all mean the same thing.
And your proof would have been a lot easier (and fun) to read if you had said:
Let $|A| = m$ and label the elements of $A$ as $\{a_1,....,a_m\}$ and let $|B|= n$ and label the elements of $B$ as $\{b_1,...,b_n\}$ so $A\times B =\{(a_i,b_j)| 1\le i \le m; 1\le j\le n\}$
By the remainder theorem we know that for every $k \in \{0,....,nm -1\}$ there are unique $p,q: 0\le p < m; 0\le q< n$ where $k= q*m + p$.  So for every $k'=k+1  \in \{1,....,nm\}$ there are $i=p+1; j=q+1$ where $k'= (j-1)m + i$.  
Thus we may define $c_{(j-1)m + i} =(a_i,b_j)$ to list $A\times B$ as $\{c_1,....., c_{nm}\}$ and we have a bijection between $A\times B$ and $[1,.....,nm]$.
