let S be comRingExtension of R; :: thesis: S is Polynom-Ring R -homomorphic
set a = the Element of S;
( hom_Ext_eval ( the Element of S,R) is additive & hom_Ext_eval ( the Element of S,R) is multiplicative & hom_Ext_eval ( the Element of S,R) is unity-preserving ) ;
hence S is Polynom-Ring R -homomorphic by RING_2:def 4; :: thesis: verum