Existence of a Basis for a Vector Space
containing a nonzero vector has a basis. Moreover, any such basis contains at most 
vectors.
Proof Given a subvector space 
of , there are two facts which, in combination, lead to a basis of .
- Given a linearly independent subset
of , there are two possibilities:
- spans in which case it is a basis of ;
- does not span in which case we can add to a vector from outside span() to obtain a larger linearly independent subset
of .
- This process of adding vectors to to obtain larger linearly independent sets stops after at most steps, because itself is spanned by vectors.
Here are the details: If 
{0}, there is nothing to show. If has nonzero vectors, pick any one such, call it a
, and form 
{a}.
We know that is linearly independent. If span() , then is a basis for . If span() 
, there are vectors in which do not belong to span(). Pick any one such, call it a
, and form 
{a}.
We know that is linearly independent. If span() , then is a basis of . If not, we form the linearly independent subset 
of by adding a vector a from but not in span() to , etc.
The crucial fact now is that, for some 
, we must have span(
) . To see this, we argue by contradiction: Suppose < and is a linearly independent subset of . Then is, in particular, a linearly independent subset of ; a contradiction to a result we obtained earlier. Thus is a basis of , and contains at most vectors.
The method of constructing a basis for a subvector space of used above can also be used to show the following refinement of the theorem above.
of , together with a linearly independent subset 
of , it is possible to select a subset 
of such that is a basis of .