Revision in response to the comments to earlier version:

To introduce the notion of a basis of a finite dimensional vector space over an arbitrary field $\Lambda$, without performing any computation on the data (any matrix manipulation, solution of a system of linear equations, Gauss elimination etc.), the following lemma can be proved:

Each $n-$frame (sequence of linearly independent vectors of length $n$) $\|e_j\|_n$ is maximal in its linear span $[\|e_j\|_n]$ (no longer frame exists in $[\|e_j\|_n]$).

From this lemma one can easily derive all the basic properties and definitions of a finite dimensional vector space including a lucid proof of the Steinitz's theorem on frame extension and many others.

This lemma is equivalent to the following proposition:

For every $n-$frame $\|f_j\|_n$, $f_i\in[\|e_j\|_n], i=1,...,n$,

$$ e_i\in[\|f_j\|_n], i=1,\ldots, n. $$

This system of inclusions can be proved by induction performed on the rank $n$ of the frame $\|e_j\|_n$. The assertion is evident for $n=1$ since in this case the linear span coincides with the family of vectors

$$ [\|e_j\|_1]=\left\{\lambda e_1|\, \lambda\in\Lambda\right\}. $$

Assuming that the assertion is proved for all natural $k\le n-1$, consider the case $k=n$. Introduce $n$ linear mappings

$$ L_i\in Hom\left([\|e_j\|_n], [\|f_1,\ldots,\hat f_i,\ldots,f_n\|]\right),\quad i=1,\ldots,n, $$

by defining $L_i$ on vectors $e_1,\ldots,e_n$ according to the equations

$$ L_ie_j=f_j,\ i\neq j,\ \ L_ie_i=0,\quad i,j=1,\ldots,n. $$

The kernel of $L_i$ coincides with the subspace

$$ ker L_i=\{\lambda e_i\bigr|\lambda\in\Lambda\}, $$

and the image --- with the linear span

$$ im\,L_i=[\|f_1,\ldots,\hat f_i,\ldots f_n\|]. $$

The restriction of $L_i$ on the subspace $[\|f_j\|_n]\subset [\|e_j\|_n]$ has a nonzero kernel since otherwise the $n$-frame $\|L_if_j\|, j=1,\ldots,n$ would be embedded in the linear span of an $(n-1)$-frame $\|f_1,\ldots,\hat f_i,\ldots,f_n\|$, which contradicts the inductive assumption. Hence,

$$ \lambda e_i\in ker L_i\Bigr|_{[\|f_j\|_n]} \ \forall\lambda\in\Lambda,\ i=1,\ldots,n, $$

or

$$ e_i\in[\|f_j\|_n]\ \forall i=1,\ldots,n. $$

The key point in this proof is that it is based on an argument much weaker than the reduction process - additionally to the list of axioms we only need the notion of the kernel of a linear mapping, without any special constructions performed on the data.

See https://arxiv.org/pdf/1712.04244.pdf for details.

A similar lemma was proved in J. Ford, Avoiding the Exchange Lemma, AMM, Vol. 102, issue 4, 1995, but the proof is based on the technique of matrix manipulations and works only with the fields of characteristic 0.

In our case, we can consider any field - finite or infinite, with any characteristic, without any calculations performed on the data.

And now the question: Is this approach already known?

By the best of my knowledge, all textbooks and articles on the subject use matrix manipulations (solution of linear equations, matrix inversion etc.) in obvious or hidden forms.

Thanks to Pietro Majer for style correction and Martin Sleziak for useful links.