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 A1: ( i in dom f & 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 jj = j + (Sum (f | (i -' 1)));
set fi = f /. i;
A2: f /. i = f . i by A1, PARTFUN1:def 8;
A3: ( i >= 1 & i <= len f ) by A1, FINSEQ_3:27;
then i -' 1 = i - 1 by XREAL_1:235;
then A4: i = (i -' 1) + 1 ;
A5: (f /. i) + (Sum (f | (i -' 1))) = Sum (f | i) by A1, A2, Lm2;
( 1 <= j & j <= f /. i ) by A1, FINSEQ_1:3;
then A6: ( 1 + 0 <= j + (Sum (f | (i -' 1))) & j + (Sum (f | (i -' 1))) <= (f /. i) + (Sum (f | (i -' 1))) ) by XREAL_1:9;
hence A7: j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) by A5; :: thesis: min f,(j + (Sum (f | (i -' 1)))) = i
i in NAT by ORDINAL1:def 13;
then ( Sum (f | i) <= Sum (f | (len f)) & f | (len f) = f ) by A3, FINSEQ_1:79, POLYNOM3:18;
then A8: Seg (Sum (f | i)) c= Seg (Sum f) by FINSEQ_1:7;
then A9: min f,(j + (Sum (f | (i -' 1)))) <= i by A5, A6, A7, Def1;
i <= min f,(j + (Sum (f | (i -' 1))))

proof

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

end;

hence min f,(j + (Sum (f | (i -' 1)))) = i by A9, XXREAL_0:1; :: thesis: verum