set B = Polynom-Ring (n,R);
defpred S₁[ object , object ] means ex a being Element of R st
( $1 = a & $2 = a | (n,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 (n,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 (n,R)) & S₁[x,y] ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in the carrier of (Polynom-Ring (n,R)) & S₁[x,y] )
then reconsider a = x as Element of R ;
reconsider y = a | (n,R) as Element of (Polynom-Ring (n,R)) by POLYNOM1:def 11;
take y ; :: thesis: ( y in the carrier of (Polynom-Ring (n,R)) & S₁[x,y] )
thus ( y in the carrier of (Polynom-Ring (n,R)) & S₁[x,y] ) ; :: thesis: verum

end;

consider g being Function of the carrier of R, the carrier of (Polynom-Ring (n,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 | (n,R)

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

end;

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