canHomP p is monomorphism ;
hence ( Polynom-Ring p is F -homomorphic & Polynom-Ring p is F -monomorphic ) by RING_3:def 3; :: thesis: verum