:: deftheorem Def1 defines finite-dimensional MATRLIN:def 1 :
for K being Field
for V being VectSp of K holds
( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );