let F be 0 -characteristic Field; :: thesis: F is F_Rat -monomorphic
take canHom_Rat F ; :: according to RING_3:def 3 :: thesis: ( canHom_Rat F is RingHomomorphism & canHom_Rat F is monomorphism )
thus ( canHom_Rat F is RingHomomorphism & canHom_Rat F is monomorphism ) ; :: thesis: verum