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
proof
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;
ex k being Nat st
( k in dom s & 0 < s . k )
proof
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;
hence 0 < Sum s by A5, RVSUM_1:85; :: thesis: verum