theorem Th81: :: REAL_NS2:81

for W being RealLinearSpace st W is finite-dimensional holds
( RLSp2RVSp W is finite-dimensional & dim (RLSp2RVSp W) = dim W )