defpred S₁[ Nat] means ( i <= Sum (f | $1) & $1 >= 1 );
A1: f | (len f) = f by FINSEQ_1:58;
A2: i <= Sum f by B1, FINSEQ_1:1;
Sum f <> 0 by B1;
then A3: len f >= 1 by FINSEQ_1:20, RVSUM_1:72;
then A4: ex k being Nat st S₁[k] by A2, A1;
consider k being Nat such that
A5: S₁[k] and
A6: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A4);
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: ( i <= Sum (f | k) & k in dom f & ( for j being Nat st i <= Sum (f | j) holds
k <= j ) )
thus i <= Sum (f | k) by A5; :: thesis: ( k in dom f & ( for j being Nat st i <= Sum (f | j) holds
k <= j ) )
k <= len f by A3, A2, A1, A6;
hence k in dom f by A5, FINSEQ_3:25; :: thesis: for j being Nat st i <= Sum (f | j) holds
k <= j
let j be Nat; :: thesis: ( i <= Sum (f | j) implies k <= j )
assume A7: i <= Sum (f | j) ; :: thesis: k <= j

per cases ( j = 0 or j > 0 ) ;

suppose j = 0 ; :: thesis: k <= j

then f | j = <*> REAL ;
hence k <= j by B1, A7, FINSEQ_1:1, RVSUM_1:72; :: thesis: verum

end;

suppose j > 0 ; :: thesis: k <= j

hence k <= j by A6, A7, NAT_1:14; :: thesis: verum

end;

end;