theorem :: REAL_NS2:82
for W being RealLinearSpace holds
( W is finite-dimensional iff RLSp2RVSp W is finite-dimensional )