let s be FinSequence of REAL ; :: thesis: ( s is nonnegative-yielding & ex i being Nat st

( i in dom s & s . i <> 0 ) implies Sum s > 0 )

assume that

A1: s is nonnegative-yielding and

A2: ex i being Nat st

( i in dom s & s . i <> 0 ) ; :: thesis: Sum s > 0

consider i being Nat such that

A3: i in dom s and

A4: s . i <> 0 by A2;

set sr = s;

A5: for j being Nat st j in dom s holds

0 <= s . j

( k in dom s & 0 < s . k )

( i in dom s & s . i <> 0 ) implies Sum s > 0 )

assume that

A1: s is nonnegative-yielding and

A2: ex i being Nat st

( i in dom s & s . i <> 0 ) ; :: thesis: Sum s > 0

consider i being Nat such that

A3: i in dom s and

A4: s . i <> 0 by A2;

set sr = s;

A5: for j being Nat st j in dom s holds

0 <= s . j

proof

ex k being Nat st
let j be Nat; :: thesis: ( j in dom s implies 0 <= s . j )

assume j in dom s ; :: thesis: 0 <= s . j

then s . j in rng s by FUNCT_1:3;

hence 0 <= s . j by A1, PARTFUN3:def 4; :: thesis: verum

end;assume j in dom s ; :: thesis: 0 <= s . j

then s . j in rng s by FUNCT_1:3;

hence 0 <= s . j by A1, PARTFUN3:def 4; :: thesis: verum

( k in dom s & 0 < s . k )

proof

hence
0 < Sum s
by A5, RVSUM_1:85; :: thesis: verum
take
i
; :: thesis: ( i in dom s & 0 < s . i )

thus i in dom s by A3; :: thesis: 0 < s . i

s . i in rng s by A3, FUNCT_1:3;

hence 0 < s . i by A1, A4, PARTFUN3:def 4; :: thesis: verum

end;thus i in dom s by A3; :: thesis: 0 < s . i

s . i in rng s by A3, FUNCT_1:3;

hence 0 < s . i by A1, A4, PARTFUN3:def 4; :: thesis: verum