set R = F;

set B = Polynom-Ring p;

defpred S_{1}[ 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_{1}[x,y] )

Z: for x being object st x in the carrier of F holds

S_{1}[x,g . x]
from FUNCT_2:sch 1(X);

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

set B = Polynom-Ring p;

defpred S

( $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

proof

consider g being Function of the carrier of F, the carrier of (Polynom-Ring p) such that
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_{1}[x,y] ) )

assume x in the carrier of F ; :: thesis: ex y being object st

( y in the carrier of (Polynom-Ring p) & S_{1}[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_{1}[x,y] )

thus ( y in the carrier of (Polynom-Ring p) & S_{1}[x,y] )
; :: thesis: verum

end;( y in the carrier of (Polynom-Ring p) & S

assume x in the carrier of F ; :: thesis: ex y being object st

( y in the carrier of (Polynom-Ring p) & S

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

thus ( y in the carrier of (Polynom-Ring p) & S

Z: for x being object st x in the carrier of F holds

S

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

then consider f being Function of F,(Polynom-Ring p) such that 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;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

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