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