@user21820: will try to work out a proof and add some details. You have to understand that linear algebra is not my forte and I am entitled to make some (silly) mistakes. But this is where you can pitch in.

@user21820: also I understand the part about span preservation. It holds for infinite sets as well.

@ParamanandSingh Ok! To clarify, I didn't intend to imply that you would make silly mistakes. The subtleties are, in fact, so subtle that mathematics professors sometimes make errors related to those as well, primarily because they do not usually write really formal proofs. That's why I'm interested to see proof attempts by you and yh05, just to make sure that both of you really understand how to do the reasoning correctly.

@ParamanandSingh Great! So you can see that the 'downward' proofs that go via removing vectors will fail in the infinite-dimensional case. (In fact, one cannot even define "dimension" without using an 'upward' construction.) This is why to prove the general theorem that every well-orderable vector space has a basis, one has to use an 'upward' construction, adding one vector on each step along the well-ordering as long as it is independent from the current set.

I will later provide a complete formal proof along these lines. I hope to see your proofs for the 'downward' algorithms first. =)

@user21820: let $S$ be a finite set of vectors with span $W$. If $S$ is linearly independent then we are done. Otherwise by definition of linear dependence we have a relation $\sum_{i=1}^{n}a_iv_i=0$ where $v_1,v_2,\dots,v_n$ are elements of $S$.

At least one of the $a_i$ say $a_k$ is non-zero. Then $v_k$ is a linear combination of all other vectors. Let $S_1=S\setminus\{v_k\}$. Then $S_1$ has same span as that of $S$. Continue the same process with $S_1$ as we did with $S$. At some point we shall reach a subset $S_j$ which is linearly independent and has same span $W$

We can do the same process bottom up. Start with any element say $v_1$ of $S$ and consider span $W_1$ of $T_1=\{v_1\}$. If $S\subseteq W_1$ then we are done. Otherwise there is some member in $S$ which is not in $W_1$ and let this member be $v_2$. Then consider span $W_2$ of set $T_2=\{v_1,v_2\}$. Note that $T_2$ is linearly independent.

If $S\subseteq W_2$ then we are done otherwise repeat the same procedure to get a linearly independent set $T_3$ with $3$ elements. In this fashion we can get a subset $T_k$ which is linearly independent and its span contains $S$ and thus has same span $W$

@ParamanandSingh For your first attempt, you need to justify "At some point we shall reach ...", which requires setting up an appropriate induction such as what I wrote.

@ParamanandSingh For your second attempt, you need to justify your last sentence, which does not follow from the previous one. Again, a suitable induction hypothesis needs to be stated and employed.

But yes, your second attempt is an 'upward' construction and the approach can be extended to infinite well-orderable S. We'll come back to that later.

@ParamanandSingh Also, taking your phrasing "say $a_k$ is non-zero" at face value, it is implicitly using the axiom of choice. That is the common subtle error that is easy to make when using your approach. That is why you must actually formalize the construction to get it right. That is, you must explicitly show how to define a sequence of vectors to be removed.

To be clear, a sequence from V of length n is a function from {1..n} to V. Can you define the sequence of removed vectors precisely?

@user21820: let me try by applying induction on number of elements of $S$. The case when $S$ has only one element is trivial as $S$ is linearly independent. Assume that the result we seek holds for all sets containing $n$ elements

And let $S$ has $n+1$ elements $v_1,v_2,\dots,v_{n+1}$

Start with $v_1$ and check is $v_1$ lies in span of $S\setminus \{v_1\}$. If yes we remove $v_1$ from $S$ to get a set of $n$ elements and by induction hypothesis our job is done. If $v_1$ is not in span of $S\setminus \{v_1\}$ then we apply the same process for $v_2$ and so on. After at most $(n+1)$ steps we have either found an element to remove or the set $S$ is linearly independent in which out job is done trivially.

And there is a useful lemma, which I will state but not prove here.

Now the proof:

Take any vector space V over F.
Let Q(k) ≡ ∀S⊆Vectors(V) ( S has size k ⇒ ∃T⊆S ( span(T) = span(S) and T is independent ) ), for each k∈ℕ.
Then Q(0) holds, because every set of 0 vectors in V is independent.
Given any k∈ℕ such that Q(k) holds:
	Given any S⊆Vectors(V) such that S has size k+1:
		If S is independent:
			S⊆S and span(S) = span(S) and S is independent.
		If S is not independent:
			Let d∈S such that d ∈ span(S∖{d}).
			Let m∈ℕ and a[1..m]∈F and x[1..m]∈S∖{d} such that d = Sum { a[i]·x[i] : i∈[1..m] }.