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