let s be FinSequence of REAL ; :: thesis: ( Sum s <> 0 implies ex i being Nat st
( i in dom s & s . i <> 0 ) )
assume A1: Sum s <> 0 ; :: thesis: ex i being Nat st
( i in dom s & s . i <> 0 )
consider n being Nat such that
A2: dom s = Seg n by FINSEQ_1:def 2;
assume for i being Nat holds
( not i in dom s or s . i = 0 ) ; :: thesis: contradiction
then for i being object st i in dom s holds
s . i = 0 ;
then A3: s = (dom s) --> 0 by FUNCOP_1:11;
s = n |-> 0 by A3, A2, FINSEQ_2:def 2;
hence contradiction by A1, RVSUM_1:81; :: thesis: verum