theorem Th8: :: TOPALG_1:8

for x, y being Real
for f being real-valued FinSequence holds (x - y) * f = (x * f) - (y * f)