Question about basis and finite dimensional vector space I have seen the statement "Every finite dimensional vector space has a basis." (Here on page 5)
I'm confused about what this tells me. It seems to tell me nothing: by definition, the dimension of a vector space is the number of elements in a basis of it. Then saying a vector space is finite dimensional is the same as saying that it has a basis.
Or are there any other definitions of dimension than the number of basis elements?
 A: Perhaps a broader context will be valuable. Let $R$ be a commutative ring (noncommutativity isn't relevant to the point I'm trying to make) and $M$ a module over it. We say that $M$ is finitely generated if there exist $m_1, ... m_n \in M$ such that every element of $M$ can be written in the form
$$m = r_1 m_1 + ... + r_n m_n.$$
When $R$ is a field $k$, an $R$-module is precisely a $k$-vector space, and a finitely generated $R$-module is precisely a finite-dimensional $k$-vector space. (Note that I can define "finite-dimensional" without defining "dimension.")
We say that $m_1, ... m_n$ is a basis of $M$ if it is a generating set which is linearly independent in the sense that if
$$0 = r_1 m_1 + ... + r_n m_n$$
then $r_1 = ... = r_n = 0$. This is equivalent to saying that each element of $M$ is uniquely expressible as a sum of the $m_i$. Abstractly, it says that the natural map
$$R^n \to M$$
given by sending $(r_1, ... r_n)$ to $r_1 m_1 + ... + r_n m_n$ is an isomorphism of $R$-modules. When $M$ has this property in module theory, we say that $M$ is a free module.
To say that every finite-dimensional vector space has a basis is to say that every finitely generated module over a field is free. It may be useful to see why this is false for more general rings: for example, a $\mathbb{Z}$-module is just an abelian group, and a $\mathbb{Z}$-module such as $\mathbb{Z}/p\mathbb{Z}$ ($p$ a prime) cannot be free. Indeed, no generating set can be linearly independent since $pm = 0$ for all $m$. 
More generally, if $R$ is a commutative ring and $I$ a nontrivial ideal of it, then $R/I$ is never free. Thus the only commutative rings $R$ for which every finitely generated module is free are those with no nontrivial ideals, and this is one of several equivalent ways to define a field. 
When $R$ is noncommutative, a more astonishing thing that can go wrong is that free modules can fail to have invariant basis number. 
A: In the document you're linking to, the following is used as the definition of finitely dimensional space.

If a vector space $V$ is spanned by a finite number of vectors, we say that it is finite dimensional.

So we do not know a priori that every finite-dimensional space (w.r.t. this definition) has a basis, we need to show this.
Only after you show that every such space has a finite basis and that any two bases have the same number elements, you can use $V$ has a basis consisting of finitely many elements as an equivalent definition of finite-dimensional space.

I think that the definition of finite-dimensional space as the space having a finite spanning set is used quite often in introductory texts on linear algebra. (Among other things, you can speak about finite-dimensional spaces before defining the notion of basis.)
IIRC I have even seen some texts where basis is assumed to have at least one element, so if you use that definition, then $\{0\}$ is an example of finite dimensional space which does not have a basis. (It is finite dimensional because it is spanned by the finite set $\{0\}$.)
Of course, if you've already mastered linear algebra, you will use any of equivalent definitions of finite-dimensional space almost automatically, details like this are important only in the introductory course, when the students encounter these notions for the first time.

EDIT: Now I noticed that this was explained already in Mark Bennet's comment above.
A: A more general definition of dimension is the maximal number of nested subspaces: a vector space $V$ has dimension $d$ if and only if $d$ is the largest number such that there exist subspaces.
$$\{0\}\subsetneq V_1\subsetneq V_2\subsetneq\cdots\subsetneq V_d=V$$
This is useful in defining dimension for more general modules.
You can in fact drop the "finite-dimensional" to get the statement that every vector space has a basis (this requires the Axiom of Choice), and then there's no problem. Or indeed, as Mark points out in the comments, the definition of "finite-dimensional" being used is that there is a finite spanning set, so the statement is telling you that the existence of a finite spanning set implies the existence of a finite basis.
