let g1, g2 be Function of (Polynom-Ring L),NAT; :: thesis: ( ( for p being Polynomial of L holds g1 . p = deg* p ) & ( for p being Polynomial of L holds g2 . p = deg* p ) implies g1 = g2 )
assume that
A1: for p being Polynomial of L holds g1 . p = deg* p and
A2: for p being Polynomial of L holds g2 . p = deg* p ; :: thesis: g1 = g2
A: dom g1 = the carrier of (Polynom-Ring L) by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom g1 holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume x in dom g1 ; :: thesis: g1 . x = g2 . x
then reconsider p = x as Polynomial of L by POLYNOM3:def 10;
thus g1 . x = deg* p by A1
.= g2 . x by A2 ; :: thesis: verum

end;

hence g1 = g2 by A; :: thesis: verum