Definition 3.1.3.  Let F be a field, V be a finite-dimensionalvector space over F. For n ∈ , we define:
dim(V) = n  :⇔  ∀ x ∈ Ba(V) : |x| = n  ⇔  ∃ x ∈ Ba(V) : |x| = n  ⇔  ∀ x ∈ V s.t. x = (V) : |x| ≥ n
Equivalence.  No proof.
Well-definedness.  No proof.
References.