i don't agree because this seems circular. You cant even define a matrix as something that acts on vectors meaningfully until you have some machinery.

if you start with a set S and then make it vector space V over field K. Then by definition, linear combinations (and its not an algebra so nonlinear isn't even defined) are closed in V.

You can then define spanning sets and linear independence to get bases. From bases you can define coordinate vectors over K^n as isomorphic to V. Then given some linear function f : V->W by definition f(v) = f(v^i * b_i) = v^i * f(b_i)

Only here is when you can even define a matrix meaningfully as a tuple of coordinate vectors which are the image of some basis vectors.

Then you need to prove that what was function application of linear functions on vectors is the same as a new operation of multiplication of matrices with coordinate vectors.

And then to prove the multiplication rule (which is inherently coordinate based) you are going make the same argument I made in sibling comment. But I could prove the rule directly by substitution using only systems of linear equations as the starting point.

Where's the circularity?

What you're saying is fine as an abstract presentation, but I was talking about how students might initially come to learn about matrices, so just introducing column vectors as representing points in 2 and 3 dimensional space and how matrices transform them is fine.

Beginning with the field and vector space axioms might be fine for sophisticated students, but I don't think it would make for an optimal learning experience for most students. We also don't teach kids the Peano axioms before they learn to add and multiply