let i be Nat; 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 ; ( 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
; 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
verumproof
assume A10:
min (
f,
(Sum (f | i)))
<> i
;
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;
verum
end;