theorem LMXFIN17: :: ASYMPT_2:35

for c, d being XFinSequence of REAL st len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) holds
for n being Nat holds (seq_p c) . n <= (seq_p d) . n