I'd be thankful for a reference to the most general form of this theorem. If I'm not mistaken, it is true that
$$ \mathcal{L}(U_n, V_m) \cong M_{m\times n}(\mathbb{F}), $$
where $U_n$ is a $n$-dimensional vector space over $\mathbb{F}$, $V_m$ is a $m$-dimensional vector space over $\mathbb{F}$, and $\mathcal{L}$ is the set of linear functions between them. My end goal is to see the formal justification for working with matrices instead of general vector spaces. I already have an intuitive grasp of it, but I'd like to understand it in detail.
What you've written is pretty much the most general form of the theorem. To prove it, the definition of dimension says you can choose bases with $m$ and $n$ elements for the domain and codomain. That coordinatization leads to the identification of linear transformations with matrices.