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 )

then - (Sum s) > 0 by RVSUM_1:88;

hence Sum s < 0 ; :: thesis: verum

( 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

then
Sum ms > 0
by a3, Th7;
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;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

then - (Sum s) > 0 by RVSUM_1:88;

hence Sum s < 0 ; :: thesis: verum