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: 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 p9 = p as Polynomial of n,L by POLYNOM1:def 27;
f . p9 = eval p9,x by A3
.= g . p9 by A4 ;
hence f . p = g . p ; :: thesis: verum

end;

A6: dom g = the carrier of (Polynom-Ring n,L) by FUNCT_2:def 1;
dom f = the carrier of (Polynom-Ring n,L) by FUNCT_2:def 1;
hence f = g by A6, A5, FUNCT_1:9; :: thesis: verum