set f = PolyHom h;

now :: thesis: for x1, x2 being object st x1 in the carrier of (Polynom-Ring R) & x2 in the carrier of (Polynom-Ring R) & (PolyHom h) . x1 = (PolyHom h) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of (Polynom-Ring R) & x2 in the carrier of (Polynom-Ring R) & (PolyHom h) . x1 = (PolyHom h) . x2 implies x1 = x2 )
assume A1: ( x1 in the carrier of (Polynom-Ring R) & x2 in the carrier of (Polynom-Ring R) & (PolyHom h) . x1 = (PolyHom h) . x2 ) ; :: thesis: x1 = x2
then reconsider p = x1, q = x2 as Element of the carrier of (Polynom-Ring R) ;

now :: thesis: for i being Element of NAT holds p . i = q . i

let i be Element of NAT ; :: thesis: p . i = q . i
h . (p . i) = ((PolyHom h) . q) . i by A1, Def2
.= h . (q . i) by Def2 ;
hence p . i = q . i by FUNCT_2:19; :: thesis: verum

end;

then p = q ;
hence x1 = x2 ; :: thesis: verum

end;

then PolyHom h is one-to-one by FUNCT_2:19;
hence PolyHom h is RingMonomorphism ; :: thesis: verum