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 A1:
( i in dom f & f . i <> 0 )
; :: thesis: min f,(Sum (f | i)) = i
then A2:
( 1 <= i & i <= len f )
by FINSEQ_3:27;
then
len (f | i) = i
by FINSEQ_1:80;
then
i in dom (f | i)
by A2, FINSEQ_3:27;
then A3:
( Sum (f | i) <= Sum (f | (len f)) & f | (len f) = f & Sum (f | i) >= (f | i) . i & (f | i) . i = f . i )
by A2, FINSEQ_1:79, FUNCT_1:70, POLYNOM3:4, POLYNOM3:18;
then
Sum (f | i) <> 0
by A1;
then
Sum (f | i) >= 1
by NAT_1:14;
then A4:
Sum (f | i) in Seg (Sum f)
by A3;
then A5:
min f,(Sum (f | i)) <= i
by Def1;
thus
min f,(Sum (f | i)) = i
:: thesis: verumproof
assume A6:
min f,
(Sum (f | i)) <> i
;
:: thesis: contradiction
then
min f,
(Sum (f | i)) < i
by A5, XXREAL_0:1;
then reconsider i1 =
i - 1 as
Element of
NAT by NAT_1:20;
min f,
(Sum (f | i)) < i1 + 1
by A6, A5, XXREAL_0:1;
then
min f,
(Sum (f | i)) <= i1
by NAT_1:13;
then
(
Sum (f | i) <= Sum (f | (min f,(Sum (f | i)))) &
Sum (f | (min f,(Sum (f | i)))) <= Sum (f | i1) )
by A4, Def1, POLYNOM3:18;
then A7:
Sum (f | i) <= Sum (f | i1)
by XXREAL_0:2;
f | (i1 + 1) = (f | i1) ^ <*(f . i)*>
by A1, FINSEQ_5:11;
then A8:
Sum (f | i) = (Sum (f | i1)) + (f . i)
by RVSUM_1:104;
then
Sum (f | i) >= Sum (f | i1)
by NAT_1:11;
then
Sum (f | i) = Sum (f | i1)
by A7, XXREAL_0:1;
hence
contradiction
by A1, A8;
:: thesis: verum
end;