theorem :: REAL_NS2:67
for X being strict RealLinearSpace holds RVSp2RLSp (RLSp2RVSp X) = X ;