theorem Th7: :: ORDERS_5:6

for s being FinSequence of REAL st s is nonnegative-yielding & ex i being Nat st
( i in dom s & s . i <> 0 ) holds
Sum s > 0