for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V
for F being FinSequence of V holds (r * L) * F = r * (L * F)