theorem :: TOPREALC:20

for f being real-valued FinSequence st |.f.| <> 0 holds
ex i being Nat st
( i in dom f & f . i <> 0 )