for V being RealLinearSpace
for a being Real
for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L