theorem NLM1: :: ASYMPT_3:6
for c being XFinSequence of REAL
for a being Real holds a (#) c is XFinSequence of REAL