for x being Real
for f, g being real-valued FinSequence holds x * (f - g) = (x * f) - (x * g) by RFUNCT_1:18;