let i, j be Nat; :: thesis: for f being FinSequence of NAT st i in dom f & j in Seg (f /. i) holds
( j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) & min (f,(j + (Sum (f | (i -' 1))))) = i )
let f be FinSequence of NAT ; :: thesis: ( i in dom f & j in Seg (f /. i) implies ( j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) & min (f,(j + (Sum (f | (i -' 1))))) = i ) )
assume that
A1: i in dom f and
A2: j in Seg (f /. i) ; :: thesis: ( j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) & min (f,(j + (Sum (f | (i -' 1))))) = i )
set fi = f /. i;
f /. i = f . i by A1, PARTFUN1:def 6;
then A3: (f /. i) + (Sum (f | (i -' 1))) = Sum (f | i) by A1, Lm2;
A4: f | (len f) = f by FINSEQ_1:58;
i <= len f by A1, FINSEQ_3:25;
then Sum (f | i) <= Sum (f | (len f)) by POLYNOM3:18;
then A5: Seg (Sum (f | i)) c= Seg (Sum f) by A4, FINSEQ_1:5;
set jj = j + (Sum (f | (i -' 1)));
j <= f /. i by A2, FINSEQ_1:1;
then A6: j + (Sum (f | (i -' 1))) <= (f /. i) + (Sum (f | (i -' 1))) by XREAL_1:7;
1 <= j by A2, FINSEQ_1:1;
then 1 + 0 <= j + (Sum (f | (i -' 1))) by XREAL_1:7;
hence A7: j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) by A3, A6; :: thesis: min (f,(j + (Sum (f | (i -' 1))))) = i
i >= 1 by A1, FINSEQ_3:25;
then i -' 1 = i - 1 by XREAL_1:233;
then A8: i = (i -' 1) + 1 ;
A9: i <= min (f,(j + (Sum (f | (i -' 1)))))

proof

assume i > min (f,(j + (Sum (f | (i -' 1))))) ; :: thesis: contradiction
then min (f,(j + (Sum (f | (i -' 1))))) <= i -' 1 by A8, NAT_1:13;
then A10: Sum (f | (min (f,(j + (Sum (f | (i -' 1))))))) <= Sum (f | (i -' 1)) by POLYNOM3:18;
0 < j by A2;
then (Sum (f | (i -' 1))) + 0 < j + (Sum (f | (i -' 1))) by XREAL_1:8;
then Sum (f | (min (f,(j + (Sum (f | (i -' 1))))))) < j + (Sum (f | (i -' 1))) by A10, XXREAL_0:2;
hence contradiction by A7, A5, Def1; :: thesis: verum

end;

min (f,(j + (Sum (f | (i -' 1))))) <= i by A3, A6, A7, A5, Def1;
hence min (f,(j + (Sum (f | (i -' 1))))) = i by A9, XXREAL_0:1; :: thesis: verum