let s be FinSequence of REAL ; :: thesis: ( s is nonpositive-yielding & ex i being Nat st
( i in dom s & s . i <> 0 ) implies Sum s < 0 )
assume that
A1: s is nonpositive-yielding and
A2: ex i being Nat st
( i in dom s & s . i <> 0 ) ; :: thesis: Sum s < 0
reconsider D = dom s as non empty set by A2;
rng s c= REAL ;
then reconsider sr = s as nonpositive-yielding Function of D,REAL by A1, FUNCT_2:2;
reconsider ms = - s as FinSequence of REAL ;
a3: ms = - sr ;
rng s c= COMPLEX by NUMBERS:11;
then reconsider sc = s as Function of D,COMPLEX by FUNCT_2:2;
A4: dom sc = dom ms by CFUNCT_1:5;
ex i being Nat st
( i in dom ms & ms . i <> 0 )

proof

consider i being Nat such that
A5: i in dom s and
A6: s . i <> 0 by A2;
take i ; :: thesis: ( i in dom ms & ms . i <> 0 )
thus i in dom ms by A5, A4; :: thesis: ms . i <> 0
assume ms . i = 0 ; :: thesis: contradiction
then - (sr . i) = 0 by A5, RFUNCT_1:58;
hence contradiction by A6; :: thesis: verum

end;

then Sum ms > 0 by a3, Th7;
then - (Sum s) > 0 by RVSUM_1:88;
hence Sum s < 0 ; :: thesis: verum