theorem TLNEG41: :: ASYMPT_2:41

for c, absc being XFinSequence of REAL st absc = |.c.| holds
for n being Nat holds |.((seq_p c) . n).| <= (seq_p absc) . n