let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S holds (PolyHom h) . (0_. R) = 0_. S
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S holds (PolyHom h) . (0_. R) = 0_. S
let h be Homomorphism of R,S; :: thesis: (PolyHom h) . (0_. R) = 0_. S
A1: 0_. R = 0. (Polynom-Ring R) by POLYNOM3:def 10;
reconsider f = (PolyHom h) . (0. (Polynom-Ring R)) as Element of the carrier of (Polynom-Ring S) ;

now :: thesis: for i being Element of NAT holds f . i = (0_. S) . i

let i be Element of NAT ; :: thesis: f . i = (0_. S) . i
f . i = h . ((0_. R) . i) by Def2, A1
.= h . (0. R) by FUNCOP_1:7
.= 0. S by RING_2:6
.= (0_. S) . i by FUNCOP_1:7 ;
hence f . i = (0_. S) . i ; :: thesis: verum

end;

hence (PolyHom h) . (0_. R) = 0_. S by A1, FUNCT_2:63; :: thesis: verum