If $W$ is a subspace of a finite dimensional vector space $V$, every linearly independent subset of $W$ is finite and is part of a (finite) basis for $W$.
Rephrasing Theorem to my taste:
If $W\leq V$, $\mathrm{dim}(V)=n\in \Bbb{N}$, $S_0\subseteq W$ is linearly independent, then $\exists B\subseteq W$ such that $B$ is a finite basis of $W$ and $S_0\subseteq B$.
Proof of first part: $S_0\subseteq W\subseteq V$ is linearly independent. By theorem 4 section 2.3, $|S_0|\leq n$. Thus $S_0$ is finite. Why Hoffman used set $S$ with $S_0\subseteq S\subseteq W$ and $S$ is independent? Is it necessary?
Proof of second part: Now we construct finite basis of $W$ from $S_0$. Let me known if I understand proof correctly, $\exists 1\leq m\leq \mathrm{dim}(V)=n$ such that $\mathrm{span}(S_m)=W$. Assume towards contradiction, $\exists m\gt n$ such that $\mathrm{span}(S_m)=W$. $S_m$ is independent by construction. By theorem 4 section 2.3, $m\leq|S_m|\leq \mathrm{dim}(V)= n$. So $m\leq n$. Which contradicts our initial assumption of $m\gt n$. Another slightly equivalent way to reach contradiction, $\exists m\gt n$ such that $\mathrm{span}(S_m)=W$. It’s easy to check $m\leq |S_m|$. So $n\lt m\leq |S_m|$. By contrapositive of theorem 4 section 2.3, $S_m$ is dependent. Thus we reach contradiction. Am I right?
Can we make argument more “concrete”? in a sense, we don’t use sentence like “if we continue in this way , then(in not more than dim$(V)$ steps) we reach a set $S_m=S_0\cup \{\beta_1,…,\beta_m\}$ which is a basis of $W$”. My Hypothesis: We claim, $\exists 1\leq m\leq \mathrm{dim}(V)$ such that $S_m=S_0\cup \{\beta_1,…,\beta_m\}$ is linearly independent and span $W$. But we haven’t defined $\{\beta_1,…,\beta_m\}$ and existence of each $\beta_i$ depends on $\beta_{i-1}$, i.e. if $\mathrm{span}(S_{i-1})\neq W$.
Edit: In hindsight, I would prove second part in following way, claim: $\exists 1\leq m\leq \mathrm{dim}(V)=n$ such that $\mathrm{span}(S_m)=W$. Proof: Assume towards contradiction, $\nexists 1\leq m\leq \mathrm{dim}(V)=n$ such that $\mathrm{span}(S_m)=W$, or equivalently $\forall 1\leq m\leq \mathrm{dim}(V)=n$ we have $\mathrm{span}(S_m)\neq W$. In particular, $\mathrm{span}(S_n)\neq W$. So $\exists \beta_{n+1}\in W$ such that $\beta_{n+1}\notin \mathrm{span}(S_n)$. $S_n=S_0 \cup \{\beta_1,…,\beta_n\}$ is linearly independent by construction. By lemma, $S_{n+1}=S_n\cup \{\beta_{n+1}\}$ is linearly independent.By theorem 4 section 2.3, $|S_{n+1}| \leq n$. But $|S_{n+1}|\geq n+1 \gt n$ by construction . Thus we reach contradiction. I think nature of both proof is different, unedited version of proof, assume $\exists m\in \Bbb{N}$ with $m\gt n$ such that $\mathrm{span}(S_m)=W$. Such $m$ may not exist, if $W$ is countable or uncountable. Edited version of proof, don’t depends on any existence. So I think is more precise.
We can make an observation, if $S_0\geq 1$, then $m\lt \mathrm{dim}(V)=n$, instead of $m\leq \mathrm{dim}(V)=n$.
Best Answer
The first paragraph is more than just proving that $S_0$ is finite. The authors are setting up the second paragraph by showing that in extending $S_0$ to a basis $S_m$ (which is an $S$) for $W$, set $S_m$ is finite and therefore can be obtained in not more than $\dim V$ steps. That is why the authors' "If we continue in this way, . . ." actually is concrete.
I read through your edited version of the proof of the second part. Your proof looks OK to me. I, however, prefer direct proofs, like the one given in the text, over proofs by contradiction.