Hello,
first of all, looking back at your algorithm it seems to me that you did not write what you intended to. In particular, all matrices and vectors were initialized to empty sequences and then updated using EXCEPT. In TLA+,
[f EXCEPT ![x] = y] = [z \in DOMAIN f |-> IF z=x THEN y ELSE f[z]]
As you can see, the domain of the function (or sequence) does not change in the update, and so all your matrices and vectors are still empty at the end. Although this does not invalidate your property, it is certainly not what you meant.
Second, `array' is really an input of the algorithm. I made it a parameter of the specification so that one can try different inputs using TLC. And it is clear that the parameters n and m should be the dimensions of the input matrix. Moreover, the way the algorithm is written makes sense only if n <= m so that we don't get out-of-bound accesses to the matrix.
All of this could have been revealed by running TLC over a few instances of your algorithm. Before you embark on a proof, it is good practice to check your specification using TLC as thoroughly as you can so that you are confident that your theorem is actually true.
Turning to the proof, I have to step back from what I said before: your correctness property is indeed inductive, but only modulo type correctness of the algorithm. I therefore stated (and model checked, but did not prove) a type correctness theorem and used it to prove your correctness property. The result is in the attached TLA+ module. Proving the typing invariant is left as an exercise, which should not be difficult.
The proof that you copied into your post is not even syntactically correct. I hope you will understand proofs better by looking at the proof in the module and at the TLAPS tutorial.
Regards,
Stephan