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

A3: now

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

end;

given j being Nat such that A5: j in dom F and
A6: 0 < F . j ; :: thesis: 0 < Sum F
((len F) |-> 0 ) . j = 0 by A2, A5, FUNCOP_1:13;
then Sum ((len F) |-> 0 ) < Sum R2 by A2, A3, A5, A6, Th113;
hence 0 < Sum F by Th111; :: thesis: verum