Interchanging two finite real sums

For $n=0$, both iterated sums are empty and equal $0$ by [F1].

Assume the identity for every $n$-by-$n$ real array, and consider an arbitrary $(n+1)$-by-$(n+1)$ array. Splitting at the last row and column and using finite-sum additivity [F1] gives ${\sum }_{j<n+1}{\sum }_{k<n+1}{a}_{jk}={\sum }_{j<n}{\sum }_{k<n}{a}_{jk}+{\sum }_{j<n}{a}_{j,n}+{\sum }_{k<n}{a}_{n,k}+a_{n,n}$. Splitting in the opposite order gives ${\sum }_{k<n+1}{\sum }_{j<n+1}{a}_{jk}={\sum }_{k<n}{\sum }_{j<n}{a}_{jk}+{\sum }_{k<n}{a}_{n,k}+{\sum }_{j<n}{a}_{j,n}+a_{n,n}$. The induction hypothesis equates the first terms, and associativity and commutativity [F3] equate the remaining sums after interchanging their order. Thus the identity holds for the successor size.

Induction [F2] using steps 1.1 and 1.2 proves the identity for every finite square array.