:: deftheorem defines RVSp2RLSp DUALSP01:def 4 :
for X being VectSp of F_Real holds RVSp2RLSp X = RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,(MultReal* X) #);