I am grappling with the following problem
Let S be a finite spanning set of $n$ vectors of a vector space V. Then V is finite dimensional and $\dim(V) \leq n$.
I have attempted to show that this holds and this is what I have now
If $S = \emptyset$, then $\operatorname{Span}(S) = V = \{0\}$ so the result is clearly true when $S$ is empty. Suppose now that S is non-empty. We will show that there is a linearly independent subset of $S$ that spans V algorithmically. If $S$ is linearly independent we are done. Otherwise we can find a vector $s_1 \in S$ such that $\operatorname{Span}(S − \{s_1\}) = V$. If $S − \{s_1\}$ is linearly independent we are done. Otherwise again we may find a vector $s_2 \in S− \{s_1\}$ such that $\operatorname{Span}(S − \{s_1,s_2\}) = V$. We continue in this manner until we finally have a linearly independent subset of $S$.
I'm not sure how to conclude that my process will end or if it is even correct. I'm fairly new to proving so I will appreciate any help, suggestions and corrections.
My line of thought for my original solution was that if we already have S to be linearly independent then we don't need to show anything. If that wern't true then we can find a vector in $S$ such if we removed it the smaller set would still span V like S. Then we apply the procedure again on the smaller set stopping if the set is linearly independent. Otherwise we continue to rip out vectors resulting in a smaller set that still spans V. I assumed that since $S$ was finite that my process would end and if it does end then we have a finite basis for $V$.
EDIT 1: I thank @Matias Heikkilä and @mathcounterexamples.net for their suggestion to reformulate my proof as an induction proof. What I have managed to produce is the following
Problem: Let V be a vector space and $S = \{s_1, s_2, \cdots, s_n\}$ where all the vectors in $S$ are distinct vectors in $V$ and $n \geq 1$ such that $\operatorname{Span}(S) = V$. Then S contains a finite basis of V.
We proceed by induction on n.
Base step ($n=1$): If $n = 1$, then $S = \{s_1\}$. If $S$ is linearly independent then $S$ forms a finite basis of V. If on the other hand $S$ is linearly dependent then $S - \{s_1\} = \emptyset$ spans $S$ which is finite and linearly independent subset that spans $V = \{0\}$. In either case we have a finite subset of $S$ that forms a basis of V. Thus our proposition holds for the base case.
Inductive step: Suppose inductively for a fixed $n > 1$ that we have have proved the result for $n -1$. We wish to show that the result holds for $n$. That is the set $S = \{s_1, s_2, \cdots, s_n\}$ contains a subset $B$ that forms a basis of V. Suppose that $S$ were linearly independent then we set $B = S$ and we are done. If on the other hand $S$ were linearly dependent then we can find a vector $v_1 \in S$ such that $\operatorname{Span}(S - \{v_1\}) = \operatorname{Span}(S) = V$. We note that $S - \{v_1\}$ is a set of $n-1$ elements which span $V$ thus we may let $S'= S - \{v_1\} $ and apply our induction hypothesis to $S'$. Whence there is a finite subset $B$ of $S'$ which forms a basis of $V$. But $B$ is also a finite subset of $S'$. Thus $S$ contains a finite subset that forms a basis of $V$. This completes the inductive step.
Conclusion: By the principle of mathematical induction, the proposition is true for all $n \geq 1$ $\Box$
Im still unsure of the validity of my original proof and the inductive proof above.