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

A1: now :: thesis: for p being object st p in the carrier of (Polynom-Ring (n,L)) holds
ex y being object st
( y in the carrier of L & S₁[p,y] )

let p be object ; :: thesis: ( p in the carrier of (Polynom-Ring (n,L)) implies ex y being object st
( y in the carrier of L & S₁[p,y] ) )
assume p in the carrier of (Polynom-Ring (n,L)) ; :: thesis: ex y being object st
( y in the carrier of L & S₁[p,y] )
then reconsider p9 = p as Polynomial of n,L by POLYNOM1:def 11;
thus ex y being object 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 object 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 11;
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