set h = the Homomorphism of R,S;
PolyHom the Homomorphism of R,S is Homomorphism of (Polynom-Ring R),(Polynom-Ring S) ;
hence Polynom-Ring S is Polynom-Ring R -homomorphic by RING_2:def 4; :: thesis: verum