theorem :: REAL_NS2:68

for X being strict VectSp of F_Real holds RLSp2RVSp (RVSp2RLSp X) = X ;