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 8;
then A3: (f /. i) + (Sum (f | (i -' 1))) = Sum (f | i) by A1, Lm2;
A4: f | (len f) = f by FINSEQ_1:79;
A5: i in NAT by ORDINAL1:def 13;
i <= len f by A1, FINSEQ_3:27;
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:7;
set jj = j + (Sum (f | (i -' 1)));
j <= f /. i by A2, FINSEQ_1:3;
then A7: j + (Sum (f | (i -' 1))) <= (f /. i) + (Sum (f | (i -' 1))) by XREAL_1:9;
1 <= j by A2, FINSEQ_1:3;
then 1 + 0 <= j + (Sum (f | (i -' 1))) by XREAL_1:9;
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:27;
then i -' 1 = i - 1 by XREAL_1:235;
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:3;
then (Sum (f | (i -' 1))) + 0 < j + (Sum (f | (i -' 1))) by XREAL_1:10;
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