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 );

now :: thesis: for x being object st x in the carrier of (Polynom-Ring F) holds
ex z being object st
( z in the carrier of (Polynom-Ring p) & S₁[x,z] )

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring F) implies ex z being object st
( z in the carrier of (Polynom-Ring p) & S₁[x,z] ) )
assume x in the carrier of (Polynom-Ring F) ; :: thesis: ex z being object st
( z in the carrier of (Polynom-Ring p) & S₁[x,z] )
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: verum

proof

take s = r mod p; :: thesis: ( s in the carrier of (Polynom-Ring p) & S₁[x,s] )
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: S₁[x,s]
take xx ; :: thesis: ( x = xx & s = xx mod p )
thus ( x = xx & s = xx mod p ) ; :: thesis: verum

end;

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: for q being Polynomial of F holds f . q = q mod p

now :: thesis: for q being Polynomial of F holds f . q = q mod p

let q be Polynomial of F; :: thesis: f . q = q mod p
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: verum

end;

hence for q being Polynomial of F holds f . q = q mod p ; :: thesis: verum