theorem :: REAL_NS2:82

for W being RealLinearSpace holds
( W is finite-dimensional iff RLSp2RVSp W is finite-dimensional )