theorem :: REAL_NS2:67

for X being strict RealLinearSpace holds RVSp2RLSp (RLSp2RVSp X) = X ;