defpred S₁[ Nat] means ( i <= Sum (f | $1) & $1 >= 1 );
A2: f | (len f) = f by FINSEQ_1:58;
A3: i <= Sum f by A1, FINSEQ_1:1;
Sum f <> 0 by A1;
then A4: len f >= 1 by FINSEQ_1:20, RVSUM_1:72;
then A5: ex k being Nat st S₁[k] by A3, A2;
consider k being Nat such that
A6: S₁[k] and
A7: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A5);
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 A6; :: thesis: ( k in dom f & ( for j being Nat st i <= Sum (f | j) holds
k <= j ) )
k <= len f by A4, A3, A2, A7;
hence k in dom f by A6, 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 A8: 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 A1, A8, RVSUM_1:72; :: thesis: verum

end;

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

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

end;

end;