theorem :: AFINSQ_2:60

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