defpred S₁[ set , set ] means ex p being Polynomial of n,R st
( p = $1 & $2 = Ext_eval (p,x) );
A1: for y being Element of the carrier of (Polynom-Ring (n,R)) ex z being Element of S st S₁[y,z]

proof

let y be Element of the carrier of (Polynom-Ring (n,R)); :: thesis: ex z being Element of S st S₁[y,z]
reconsider p = y as Polynomial of n,R by POLYNOM1:def 11;
take Ext_eval (p,x) ; :: thesis: S₁[y, Ext_eval (p,x)]
take p ; :: thesis: ( p = y & Ext_eval (p,x) = Ext_eval (p,x) )
thus ( p = y & Ext_eval (p,x) = Ext_eval (p,x) ) ; :: thesis: verum

end;

consider f being Function of (Polynom-Ring (n,R)),S such that
A2: for y being Element of (Polynom-Ring (n,R)) holds S₁[y,f . y] from FUNCT_2:sch 3(A1);
reconsider f = f as Function of (Polynom-Ring (n,R)),S ;
take f ; :: thesis: for p being Polynomial of n,R holds f . p = Ext_eval (p,x)
let p be Polynomial of n,R; :: thesis: f . p = Ext_eval (p,x)
p in Polynom-Ring (n,R) by POLYNOM1:def 11;
then ex q being Polynomial of n,R st
( q = p & f . p = Ext_eval (q,x) ) by A2;
hence f . p = Ext_eval (p,x) ; :: thesis: verum