let F be p -characteristic Field; :: thesis: F is Z/ p -monomorphic
take canHom_Z/ (p,F) ; :: according to RING_3:def 3 :: thesis: ( canHom_Z/ (p,F) is RingHomomorphism & canHom_Z/ (p,F) is monomorphism )
thus ( canHom_Z/ (p,F) is RingHomomorphism & canHom_Z/ (p,F) is monomorphism ) ; :: thesis: verum