set R = F;
set B = Polynom-Ring p;
defpred S₁[ object , object ] means ex a being Element of F st
( $1 = a & $2 = a | F );
X: for x being object st x in the carrier of F holds
ex y being object st
( y in the carrier of (Polynom-Ring p) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of F implies ex y being object st
( y in the carrier of (Polynom-Ring p) & S₁[x,y] ) )
assume x in the carrier of F ; :: thesis: ex y being object st
( y in the carrier of (Polynom-Ring p) & S₁[x,y] )
then reconsider a = x as Element of F ;
( not deg p <= 0 & deg (a | F) <= 0 ) by RING_4:def 4, RATFUNC1:def 2;
then a | F in { q where q is Polynomial of F : deg q < deg p } ;
then reconsider y = a | F as Element of (Polynom-Ring p) by RING_4:def 8;
take y ; :: thesis: ( y in the carrier of (Polynom-Ring p) & S₁[x,y] )
thus ( y in the carrier of (Polynom-Ring p) & S₁[x,y] ) ; :: thesis: verum

end;

consider g being Function of the carrier of F, the carrier of (Polynom-Ring p) such that
Z: for x being object st x in the carrier of F holds
S₁[x,g . x] from FUNCT_2:sch 1(X);

now :: thesis: for x being Element of F holds g . x = x | F

let x be Element of F; :: thesis: g . x = x | F
consider a being Element of F such that
H: ( x = a & g . x = a | F ) by Z;
thus g . x = x | F by H; :: thesis: verum

end;

then consider f being Function of F,(Polynom-Ring p) such that
Y: for x being Element of F holds f . x = x | F ;
take f ; :: thesis: for a being Element of F holds f . a = a | F
thus for a being Element of F holds f . a = a | F by Y; :: thesis: verum