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