theorem Th60: :: AFINSQ_2:61

for rF being real-valued XFinSequence
for r being Real st rF is nonnegative-yielding & len rF > 0 & ex x being object st
( x in dom rF & rF . x = r ) holds
Sum rF >= r