for f1, f2 being Real_Sequence
for n being non trivial Nat st ( for k being non trivial Nat st k <= n holds
f1 . k < f2 . k ) holds
Sum (f1,n,1) < Sum (f2,n,1)