theorem :: RLAFFIN1:25

for r, s being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)