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 :: thesis: for p being object st p in the carrier of (Polynom-Ring (n,L)) holds
f . p = g . p

let p be object ; :: 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 11;
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:2; :: thesis: verum