take |. the INT -valued Polynomial of n,F_Real.| ; :: thesis: |. the INT -valued Polynomial of n,F_Real.| is natural-valued
thus |. the INT -valued Polynomial of n,F_Real.| is natural-valued ; :: thesis: verum