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 )

F . i = 0. R ; :: thesis: F is finite-Support

Support F c= Segm n

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

given n being Nat such that A6:
for i being Nat st i >= n holds
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

end;for i being Nat st i >= n holds

F . i = 0. R

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

end;

suppose A2:
Support F = {}
; :: thesis: ex n being Nat st

for i being Nat st i >= n holds

F . i = 0. R

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;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

suppose
Support F <> {}
; :: thesis: ex n being Nat st

for i being Nat st i >= n holds

F . i = 0. R

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;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

F . i = 0. R ; :: thesis: F is finite-Support

Support F c= Segm n

proof

hence
Support F is finite
; :: according to POLYNOM1:def 5 :: thesis: verum
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;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