theorem Lm02: :: DUALSP01:2

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