f in [#] (Polynom-Ring (n,L)) by SUBSET_1:def 1;
then f is Polynomial of n,L by POLYNOM1:def 11;
then reconsider p = f as Polynomial of n,L ;
consider y being Element of L such that
A1: y = eval (p,x) ;
thus ex b₁ being Element of L ex p being Polynomial of n,L st
( p = f & b₁ = eval (p,x) ) by A1; :: thesis: verum