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

( 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