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