A: ( canHom R is additive & canHom R is multiplicative & canHom R is unity-preserving & canHom R is monomorphism ) ;
hence Polynom-Ring R is R -homomorphic by RING_2:def 4; :: thesis: Polynom-Ring R is R -monomorphic
thus Polynom-Ring R is R -monomorphic by A, RING_3:def 3; :: thesis: verum