let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S holds (PolyHom h) . (1_. R) = 1_. S
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S holds (PolyHom h) . (1_. R) = 1_. S
let h be Homomorphism of R,S; :: thesis: (PolyHom h) . (1_. R) = 1_. S
thus (PolyHom h) . (1_. R) = (PolyHom h) . (1_ (Polynom-Ring R)) by POLYNOM3:def 10
.= 1_ (Polynom-Ring S) by GROUP_1:def 13
.= 1_. S by POLYNOM3:def 10 ; :: thesis: verum