Row rank equals column rank

For every type $K$ (in an arbitrary universe) carrying a field structure, for every pair of natural numbers $m$ and $n$ (both left implicit, so the claim ranges over all of $\mathbb{N} \times \mathbb{N}$, including $m = 0$ and/or $n = 0$), and for every matrix $A$ with rows indexed by $\{0,\dots,m-1\}$ and columns indexed by $\{0,\dots,n-1\}$ and entries in $K$ — formally, $A$ is a function assigning to each row index $i$ and column index $j$ a scalar $A_{i,j} \in K$ — the statement asserts the equality of two dimensions:

where the two sides are taken in different ambient spaces. On the left, $A_i$ denotes the $i$-th row of $A$ regarded as the function $j \mapsto A_{i,j}$, i.e. a vector of the $K$-vector space $K^n$ of functions from the index set $\{0,\dots,n-1\}$ to $K$; the spanned set is literally the image of the map $i \mapsto A_i$, that is, the set of all vectors of $K^n$ arising as some row of $A$ (a set, so repeated identical rows contribute only once, which does not affect the span), and the span is the $K$-linear subspace of $K^n$ it generates. On the right, $A^{\mathsf T}$ is the transposed matrix, with rows indexed by $\{0,\dots,n-1\}$ and columns by $\{0,\dots,m-1\}$ and entries $A^{\mathsf T}_{j,i} = A_{i,j}$; $A^{\mathsf T}_j$ denotes its $j$-th row, i.e. the $j$-th column of $A$ regarded as the function $i \mapsto A_{i,j}$, a vector of the $K$-vector space $K^m$; the spanned set is the image of the map $j \mapsto A^{\mathsf T}_j$, i.e. the set of all vectors of $K^m$ arising as some column of $A$, and the span is the $K$-linear subspace of $K^m$ it generates. Each side is the finite-dimensional rank invariant of the corresponding subspace, viewed as a $K$-vector space in its own right, and this invariant is by convention $0$ for any module that is not finite-dimensional (a case that cannot arise here, since both subspaces sit inside finite-dimensional spaces). Both sides are compared as natural numbers, so the assertion is an equality in $\mathbb{N}$, not merely an inequality in either direction, and it carries no nondegeneracy hypothesis on $A$: the zero matrix, and the degenerate shapes where $m = 0$ (the left-hand set is empty, its span the zero subspace of $K^n$, while the right-hand set consists of the $n$ columns, each the unique element of the zero space $K^0$) or $n = 0$ (symmetrically), are all included in the claim. No hypotheses beyond "$K$ is a field" are assumed — in particular nothing about the characteristic, cardinality, or decidability of $K$ — and $A$ is the only explicit argument. The declaration is stated with its proof left as a placeholder.