take 1_. F_Rat ; :: thesis: ( 1_. F_Rat is monic & 1_. F_Rat is INT -valued )
thus ( 1_. F_Rat is monic & 1_. F_Rat is INT -valued ) ; :: thesis: verum