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