Interchange of a Finite Double Sum

Let $K$ be a \reftext{def:field-c54-2026b}{field}, let $m,n$ be \reftext{def:natural-numbers-2026a}{natural numbers}, and let $[m]$ and $[n]$ be the \reftext{def:initial-segment-natural-numbers-2026a}{initial segments} they determine. Let $a\in(K^{n})^{m}$ be an \reftext{def:finite-tuple-power-2026a}{$m$-tuple} of $n$-tuples in $K$, with components $(a_{j})_{k}$ for $j\in[m]$ and $k\in[n]$, and let $b\in K^{m}$ and $c\in K^{n}$ be given by the \reftext{def:finite-sum-field-2026b}{finite sums}

Then

written in abbreviated form as