set B = Polynom-Ring F;
set D = the carrier of (Polynom-Ring F);
defpred S₁[ object , object ] means ex q being Element of the carrier of (Polynom-Ring F) st
( $1 = q & $2 = q mod p );

let x be object ; :: thesis:
assume x in the carrier of (Polynom-Ring F) ; :: thesis:
then reconsider xx = x as Element of the carrier of (Polynom-Ring F) ;
reconsider r = xx as Polynomial of F ;
thus ex z being object st
( z in the carrier of (Polynom-Ring p) & S₁[x,z] ) :: thesis:

take s = r mod p; :: thesis:
deg s < deg p by RING_2:29;
then s in { q where q is Polynomial of F : deg q < deg p } ;
hence s in the carrier of (Polynom-Ring p) by defprfp; :: thesis:
take xx ; :: thesis:
thus ( x = xx & s = xx mod p ) ; :: thesis:

end;

then I: for x being object st x in the carrier of (Polynom-Ring F) holds
ex y being object st
( y in the carrier of (Polynom-Ring p) & S₁[x,y] ) ;
consider f being Function of the carrier of (Polynom-Ring F),(Polynom-Ring p) such that
H: for x being object st x in the carrier of (Polynom-Ring F) holds
S₁[x,f . x] from FUNCT_2:sch 1(I);
reconsider f = f as Function of (Polynom-Ring F),(Polynom-Ring p) ;
take f ; :: thesis:

let q be Polynomial of F; :: thesis:
q in Polynom-Ring F by POLYNOM3:def 10;
then S₁[q,f . q] by H;
then consider qq being Element of the carrier of (Polynom-Ring F) such that
K: ( qq = q & f . qq = qq mod p ) ;
thus f . q = q mod p by K; :: thesis:

end;