let i be Nat; :: thesis: for f being FinSequence of NAT st i in dom f & f . i <> 0 holds
min (f,(Sum (f | i))) = i
let f be FinSequence of NAT ; :: thesis: ( i in dom f & f . i <> 0 implies min (f,(Sum (f | i))) = i )
assume that
A1: i in dom f and
A2: f . i <> 0 ; :: thesis: min (f,(Sum (f | i))) = i
A3: i <= len f by A1, FINSEQ_3:25;
then A4: len (f | i) = i by FINSEQ_1:59;
1 <= i by A1, FINSEQ_3:25;
then A5: i in dom (f | i) by A4, FINSEQ_3:25;
then Sum (f | i) >= (f | i) . i by POLYNOM3:4;
then Sum (f | i) <> 0 by A2, A5, FUNCT_1:47;
then A6: Sum (f | i) >= 1 by NAT_1:14;
A7: f | (len f) = f by FINSEQ_1:58;
Sum (f | i) <= Sum (f | (len f)) by A3, POLYNOM3:18;
then A8: Sum (f | i) in Seg (Sum f) by A7, A6;
then A9: min (f,(Sum (f | i))) <= i by Def1;
thus min (f,(Sum (f | i))) = i :: thesis: verum

proof

assume A10: min (f,(Sum (f | i))) <> i ; :: thesis: contradiction
then min (f,(Sum (f | i))) < i by A9, XXREAL_0:1;
then reconsider i1 = i - 1 as Element of NAT by NAT_1:20;
min (f,(Sum (f | i))) < i1 + 1 by A9, A10, XXREAL_0:1;
then min (f,(Sum (f | i))) <= i1 by NAT_1:13;
then A11: Sum (f | (min (f,(Sum (f | i))))) <= Sum (f | i1) by POLYNOM3:18;
Sum (f | i) <= Sum (f | (min (f,(Sum (f | i))))) by A8, Def1;
then A12: Sum (f | i) <= Sum (f | i1) by A11, XXREAL_0:2;
f | (i1 + 1) = (f | i1) ^ <*(f . i)*> by A1, FINSEQ_5:10;
then A13: Sum (f | i) = (Sum (f | i1)) + (f . i) by RVSUM_1:74;
then Sum (f | i) >= Sum (f | i1) by NAT_1:11;
then Sum (f | i) = Sum (f | i1) by A12, XXREAL_0:1;
hence contradiction by A2, A13; :: thesis: verum

end;