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 )
set B = the Basis of V;
assume [#] V is finite ; :: thesis: V is finite-dimensional
then reconsider B = the Basis of V as finite Subset of V ;
take B ; :: according to MATRLIN:def 1 :: thesis: B is Element of K16( the carrier of V)
thus B is Element of K16( the carrier of V) ; :: thesis: verum