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

proof

let y be Element of the carrier of (Polynom-Ring A); :: thesis: ex z being Element of B st S₁[y,z]
reconsider p = y as Polynomial of A ;
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 A),B such that
A2: for y being Element of (Polynom-Ring A) holds S₁[y,f . y] from FUNCT_2:sch 3(A1);
reconsider f = f as Function of (Polynom-Ring A),B ;
take f ; :: thesis: for p being Polynomial of A holds f . p = Ext_eval (p,x)
let p be Polynomial of A; :: thesis: f . p = Ext_eval (p,x)
p in Polynom-Ring A by POLYNOM3:def 10;
then ex q being Polynomial of A st
( q = p & f . p = Ext_eval (q,x) ) by A2;
hence f . p = Ext_eval (p,x) ; :: thesis: verum