theorem NLM4: :: ASYMPT_3:9

for c, c1 being non empty positive-yielding XFinSequence of REAL
for a being Real st c1 = a (#) c holds
for x being Nat holds (polynom c1) . x = a * ((polynom c) . x)