let B be Basis of V; :: thesis: not B is empty
dim V <> 0 by MATRLIN2:42;
then card B <> 0 by VECTSP_9:def 1;
hence not B is empty ; :: thesis: verum