defpred S1[ 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 S1[y,z]
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 S1[y,f . y]
from FUNCT_2:sch 3(A1);
reconsider f = f as Function of (Polynom-Ring L),L ;
take
f
; for p being Polynomial of L holds f . p = eval (p,x)
let p be Polynomial of L; 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)
; verum