take <*> the carrier of F_Real ; :: thesis: <*> the carrier of F_Real is INT -valued
thus <*> the carrier of F_Real is INT -valued ; :: thesis: verum