matrix

Matrix

context	$X$ … set
context	$n,m\in \mathbb N$
definiendum	$A\in \mathrm{Matrix}(n,m,X)$
postulate	$A\in\mathrm{FinSequence}(\mathrm{FinSequence}(X))$
range	$1\ge i\ge m$
postulate	$\mathrm{length}(A)=n$
postulate	$\mathrm{length}(A_i)=m$

We write

$A_{ij}\equiv (A_i)_j$