theorem :: RLVECT_2:61

for V being RealLinearSpace holds the Mult of (LC_RLSpace V) = LCMult V ;