thus ( F is finite-Support implies ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R ) :: thesis: ( ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R implies F is finite-Support )

proof

assume A1: Support F is finite ; :: according to POLYNOM1:def 5 :: thesis: ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R

per cases ( Support F = {} or Support F <> {} ) ;

suppose A2: Support F = {} ; :: thesis: ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R

take 0 ; :: thesis: for i being Nat st i >= 0 holds
F . i = 0. R
let i be Nat; :: thesis: ( i >= 0 implies F . i = 0. R )
assume i >= 0 ; :: thesis: F . i = 0. R
assume A3: F . i <> 0. R ; :: thesis: contradiction
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i in Support F by A3, POLYNOM1:def 4;
hence contradiction by A2; :: thesis: verum

end;

suppose Support F <> {} ; :: thesis: ex n being Nat st
for i being Nat st i >= n holds
F . i = 0. R

then reconsider A = Support F as non empty finite Subset of NAT by A1;
take n = (max A) + 1; :: thesis: for i being Nat st i >= n holds
F . i = 0. R
let i be Nat; :: thesis: ( i >= n implies F . i = 0. R )
assume i >= n ; :: thesis: F . i = 0. R
then A4: i > max A by NAT_1:13;
assume A5: F . i <> 0. R ; :: thesis: contradiction
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i in Support F by A5, POLYNOM1:def 4;
hence contradiction by A4, XXREAL_2:def 8; :: thesis: verum

end;

end;

end;

given n being Nat such that A6: for i being Nat st i >= n holds
F . i = 0. R ; :: thesis: F is finite-Support
Support F c= Segm n

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Support F or e in Segm n )
assume A7: e in Support F ; :: thesis: e in Segm n
then reconsider i = e as Nat ;
F . i <> 0. R by A7, POLYNOM1:def 3;
hence e in Segm n by A6, NAT_1:44; :: thesis: verum

end;

hence Support F is finite ; :: according to POLYNOM1:def 5 :: thesis: verum