defpred S₁[ set , set ] means ex p9 being Polynomial of n,L st
( p9 = $1 & $2 = eval p9,x );

A1: now

let p be set ; :: thesis: ( p in the carrier of (Polynom-Ring n,L) implies ex y being set st
( y in the carrier of L & S₁[p,y] ) )
assume p in the carrier of (Polynom-Ring n,L) ; :: thesis: ex y being set st
( y in the carrier of L & S₁[p,y] )
then reconsider p9 = p as Polynomial of n,L by POLYNOM1:def 27;
thus ex y being set st
( y in the carrier of L & S₁[p,y] ) :: thesis: verum

proof

take eval p9,x ; :: thesis: ( eval p9,x in the carrier of L & S₁[p, eval p9,x] )
thus ( eval p9,x in the carrier of L & S₁[p, eval p9,x] ) ; :: thesis: verum

end;

end;

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