theorem Th2: :: NEWTON:2

for a being Real
for F being FinSequence of REAL holds len (a * F) = len F