for f, g being Real_Sequence
for N being Element of NAT st ( for n being Element of NAT st n <= N holds
f . n <= g . n ) holds
Sum (f,N) <= Sum (g,N) by Lm13;