for F being sequence of ExtREAL st F is nonnegative holds
for n, m being Nat holds (Ser F) . n <= (Ser F) . (n + m)