Construction of matrices under ZFC axioms

Do anybody know how matrices are built into ZFC theory ? I pretty have no idea how to build them from ZFC axioms. I would like a constructive proof of their existence if possible.

Lets talk about matrices with real entries. If you are okay with the construction of the reals $\Bbb R$ and the construction of cartesian products $M\times N$ of subsets of natural numbers $M=\{1,...,m\}$ and $N=\{1,...,n\}$, then a $(m\times n)$-matrix $A%$ is nothing more than just a map
$$A\quad:\quad M\times N\to \Bbb R,\quad (i,j)\mapsto A_{ij}$$
• @toto Essentially for sets $X,Y$ we can define $X\times Y$ as some special subset of $\mathcal P(\mathcal P(X\cup Y)$. But you can probably find this already asked here on Math.SE, e.g. here. – M. Winter Jun 13 '17 at 9:57
• @toto As matrices are consideres as maps, matrix operations are consideres as maps that map maps to other maps (oh god, sounds terrible). E.g. the transpose might be something like this $$\cdot^\top\quad:\quad\mathrm{Func}(M\times N, \Bbb R)\to\mathrm{Func}(M\times N, \Bbb R),\quad (\cdot^\top)(A)(i,j)=A_{ji}.$$ I do not know what your distinction is between application and algorithm. – M. Winter Jun 13 '17 at 9:59