let F be Field; :: thesis: for V being VectSp of F st [#] V is finite holds
V is finite-dimensional
let V be VectSp of F; :: thesis: ( [#] V is finite implies V is finite-dimensional )
assume A1: [#] V is finite ; :: thesis: V is finite-dimensional
consider B being Basis of V;
reconsider B = B as finite Subset of V by A1;
take B ; :: according to MATRLIN:def 3 :: thesis: B is Basis of V
thus B is Basis of V ; :: thesis: verum