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