:: deftheorem defines RLSp2RVSp DUALSP01:def 2 :
for X being RealLinearSpace holds RLSp2RVSp X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #);