@user21820: well the basis is not unique so we can remove those vectors which can be expressed as linear combination of other vectors. Since we have begun with finite number of vectors this must end somewhere.
However implementing this scheme as an algorithm needs something equivalent to reducing matrices in echelon form.
I think a crucial part which needs to proved is that if some finite set $S$ of vectors has a span $W$ and $v$ is a linear combination of vectors in $S$ then $S_1=S\cup \{v\} $ also has the same span $W$. But this should not be difficult to prove.
@ParamanandSingh No you cannot simply remove every vector which is a linear combination of the others, otherwise if you start with {v,2·v} then you will remove both. That is the reason the algorithm must proceed in steps.
@ParamanandSingh What you stated is correct even if S is not finite. Indeed it is easy to prove. But since it does not require S to be finite, it actually shows that it is not the core of the fact we wish to prove here, because what we want to prove requires induction and fails if you start with an infinite set of vectors that are not independent. In particular, if you start with the infinite set { k·v : k∈ℤ } where v≠0, then removing one linearly dependent vector at a time will never finish.
@ParamanandSingh Note that the induction idea I gave above is specific to the algorithm given in the quoted text. If I amend your first sentence to "... we can remove on each step some vector that can be expressed as a linear combination ...", then it becomes a different algorithm. To prove yours correct, your induction must be slightly more powerful:
> Again induct along the steps, namely show that after k steps the span of the remaining list is span(V) and is either linearly independent or has size #(V)−k.
From this you can deduce that the remaining list becomes independent within #(V) steps, otherwise after that it has size 0.
I'm not giving all the details, so you should try to work it out. By the way, it may seem as if your approach is inferior to the quoted text because the induction argument needed is more complicated, but that is not the case. Although the approach in the quoted text has a simpler induction argument (also called a loop-invariant) for the preservation of span, one must also prove by induction that each vector that remains is not in the span of preceding vectors in the list!
@yh05: Especially take note of my last comment above. That is, the text you quoted failed to provide a proper proof of two properties of the given algorithm. Both of them requires induction (though of course you are free to lump them together and use a single induction to prove both).
