theorem Lm01: :: DUALSP01:1

for X being RealLinearSpace holds ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(MultF_Real* X) #) is VectSp of F_Real