let F be real-valued FinSequence; :: thesis: ( ( for i being Nat st i in dom F holds
0 <= F . i ) implies 0 <= Sum F )
reconsider F1 = F as FinSequence of REAL by Lm2;
set i = len F;
set R1 = (len F) |-> (In (0,REAL));
reconsider R2 = F1 as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: Seg (len F) = dom F by FINSEQ_1:def 3;
assume A2: for i being Nat st i in dom F holds
0 <= F . i ; :: thesis: 0 <= Sum F
for j being Nat st j in Seg (len F) holds
((len F) |-> (In (0,REAL))) . j <= R2 . j

proof

let j be Nat; :: thesis: ( j in Seg (len F) implies ((len F) |-> (In (0,REAL))) . j <= R2 . j )
assume A3: j in Seg (len F) ; :: thesis: ((len F) |-> (In (0,REAL))) . j <= R2 . j
((len F) |-> (In (0,REAL))) . j = In (0,REAL) ;
hence ((len F) |-> (In (0,REAL))) . j <= R2 . j by A2, A1, A3; :: thesis: verum

end;

then Sum ((len F) |-> (In (0,REAL))) <= Sum R2 by Th82;
hence 0 <= Sum F by Th81; :: thesis: verum