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

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