theorem NLM2: :: ASYMPT_3:7

for c being non empty positive-yielding XFinSequence of REAL
for a being Real st 0 < a holds
a (#) c is non empty positive-yielding XFinSequence of REAL