set f = poly_mod p;

now :: thesis: for x being object st x in the carrier of (Polynom-Ring p) holds
x in rng (poly_mod p)

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring p) implies x in rng (poly_mod p) )
assume x in the carrier of (Polynom-Ring p) ; :: thesis: x in rng (poly_mod p)
then x in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider q being Polynomial of F such that
B: ( q = x & deg q < deg p ) ;
q mod p = q by B, div1;
then C: (poly_mod p) . x = q by B, dpm;
dom (poly_mod p) = the carrier of (Polynom-Ring F) by FUNCT_2:def 1;
then q in dom (poly_mod p) by POLYNOM3:def 10;
hence x in rng (poly_mod p) by B, C, FUNCT_1:def 3; :: thesis: verum

end;

then for x being object holds
( x in rng (poly_mod p) iff x in the carrier of (Polynom-Ring p) ) ;
hence poly_mod p is onto by FUNCT_2:def 3, TARSKI:2; :: thesis: verum