canHomP p is monomorphism
;

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

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