theorem Th2: :: NEWTON:2

for a being Real
for F being real-valued FinSequence holds len (a * F) = len F