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 12;
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 12;
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