defpred S₁[ Nat] means ( i <= Sum (f | $1) & $1 >= 1 );
A2: ( len f >= 1 & i <= Sum f & f | (len f) = f ) by A1, FINSEQ_1:3, FINSEQ_1:4, FINSEQ_1:28, FINSEQ_1:79, RVSUM_1:102;
then A3: ex k being Nat st S₁[k] ;
consider k being Nat such that
A4: S₁[k] and
A5: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A3);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
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 A4; :: thesis: ( k in dom f & ( for j being Nat st i <= Sum (f | j) holds
k <= j ) )
k <= len f by A5, A2;
hence k in dom f by A4, FINSEQ_3:27; :: 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 A6: 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, A6, FINSEQ_1:3, RVSUM_1:102; :: thesis: verum

end;

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

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

end;

end;