theorem :: NEWTON:3
for a being Real
for F being real-valued FinSequence holds dom F = dom (a * F) by VALUED_1:def 5;