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

proof

let y be Element of (Polynom-Ring L); :: thesis: ex z being Element of L st S₁[y,z]
reconsider p = y as Polynomial of L by POLYNOM3:def 10;
take eval (p,x) ; :: thesis: S₁[y, eval (p,x)]
take p ; :: thesis: ( p = y & eval (p,x) = eval (p,x) )
thus ( p = y & eval (p,x) = eval (p,x) ) ; :: thesis: verum

end;

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