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

proof

let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st
( y in the carrier of (Polynom-Ring R) & S₁[x,y] ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in the carrier of (Polynom-Ring R) & S₁[x,y] )
then reconsider a = x as Element of R ;
reconsider y = a | R as Element of (Polynom-Ring R) by POLYNOM3:def 10;
take y ; :: thesis: ( y in the carrier of (Polynom-Ring R) & S₁[x,y] )
thus ( y in the carrier of (Polynom-Ring R) & S₁[x,y] ) ; :: thesis: verum

end;

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

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

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

end;

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