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;
A5: i in NAT by ORDINAL1:def 12;
i <= len f by A1, FINSEQ_3:25;
then Sum (f | i) <= Sum (f | (len f)) by A5, POLYNOM3:18;
then A6: 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 A7: 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 A8: j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) by A3, A7; :: 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 A9: i = (i -' 1) + 1 ;
A10: 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 A9, NAT_1:13;
then A11: Sum (f | (min (f,(j + (Sum (f | (i -' 1))))))) <= Sum (f | (i -' 1)) by POLYNOM3:18;
0 < j by A2, FINSEQ_1:1;
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 A11, XXREAL_0:2;
hence contradiction by A8, A6, Def1; :: thesis: verum

end;

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