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