let F be 0 -characteristic Field; :: thesis: F_Rat , PrimeField F are_isomorphic
take canHom_Rat (PrimeField F) ; :: according to QUOFIELD:def 23 :: thesis: canHom_Rat (PrimeField F) is isomorphism
thus canHom_Rat (PrimeField F) is isomorphism ; :: thesis: verum