for rF being real-valued XFinSequence
for r being Real st ( for n being Nat st n in dom rF holds
rF . n <= r ) holds
Sum rF <= (len rF) * r