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 ;
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 ;
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 ;
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:
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 ;
hence e in Segm n by ; :: thesis: verum
end;
hence Support F is finite ; :: according to POLYNOM1:def 5 :: thesis: verum