let F be Field; :: thesis:
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis:
set R = Polynom-Ring F;
set S = Polynom-Ring p;
set f = poly_mod p;
reconsider p1 = p as Element of (Polynom-Ring F) ;

A: now :: thesis:

let x be object ; :: thesis:
assume A0: x in ker (poly_mod p) ; :: thesis:
then x in { v where v is Element of (Polynom-Ring F) : (poly_mod p) . v = 0. (Polynom-Ring p) } by VECTSP10:def 9;
then consider y being Element of (Polynom-Ring F) such that
A1: ( y = x & (poly_mod p) . y = 0. (Polynom-Ring p) ) ;
reconsider q = x as Element of the carrier of (Polynom-Ring F) by A0;
reconsider q1 = x as Element of (Polynom-Ring F) by A0;
A2: q - ((q div p) *' p) = q mod p
.= 0. (Polynom-Ring p) by A1, dpm
.= 0_. F by defprfp ;
reconsider qp = q div p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
qp * p1 = (q div p) *' p by POLYNOM3:def 10;
then A3: - (qp * p1) = - ((q div p) *' p) by lemminuspoly;
q1 - (qp * p1) = q + (- ((q div p) *' p)) by A3, POLYNOM3:def 10
.= 0. (Polynom-Ring F) by A2, POLYNOM3:def 10 ;
then qp * p1 = q1 by RLVECT_1:21;
then q in { (p * r) where r is Element of (Polynom-Ring F) : verum } ;
hence x in {p} -Ideal by IDEAL_1:64; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume x in {p} -Ideal ; :: thesis:
then x in { (p * r) where r is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;
then consider y being Element of (Polynom-Ring F) such that
A1: x = p * y ;
reconsider q = y as Element of the carrier of (Polynom-Ring F) ;
p * y = p *' q by POLYNOM3:def 10;
then (poly_mod p) . x = (p *' q) mod p by A1, dpm
.= 0_. F by T2, div2
.= 0. (Polynom-Ring p) by defprfp ;
then x in { v where v is Element of (Polynom-Ring F) : (poly_mod p) . v = 0. (Polynom-Ring p) } by A1;
hence x in ker (poly_mod p) by VECTSP10:def 9; :: thesis:

end;

hence ker (poly_mod p) = {p} -Ideal by A, TARSKI:2; :: thesis: