let f, g be Function of (Polynom-Ring n,L),L; :: thesis: ( ( for p being Polynomial of n,L holds f . p = eval p,x ) & ( for p being Polynomial of n,L holds g . p = eval p,x ) implies f = g )
assume that
A3: for p being Polynomial of n,L holds f . p = eval p,x and
A4: for p being Polynomial of n,L holds g . p = eval p,x ; :: thesis: f = g
reconsider f = f, g = g as Function of the carrier of (Polynom-Ring n,L),the carrier of L ;
A5: ( dom f = the carrier of (Polynom-Ring n,L) & dom g = the carrier of (Polynom-Ring n,L) ) by FUNCT_2:def 1;

now

let p be set ; :: thesis: ( p in the carrier of (Polynom-Ring n,L) implies f . p = g . p )
assume p in the carrier of (Polynom-Ring n,L) ; :: thesis: f . p = g . p
then reconsider p' = p as Polynomial of n,L by POLYNOM1:def 27;
f . p' = eval p',x by A3
.= g . p' by A4 ;
hence f . p = g . p ; :: thesis: verum

end;

hence f = g by A5, FUNCT_1:9; :: thesis: verum