set R = Polynom-Ring L;
defpred S₁[ object , object ] means ex p being Polynomial of L st
( $1 = p & $2 = deg* p );
A: for x being object st x in the carrier of (Polynom-Ring L) holds
ex y being object st
( y in NAT & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring L) implies ex y being object st
( y in NAT & S₁[x,y] ) )
assume x in the carrier of (Polynom-Ring L) ; :: thesis: ex y being object st
( y in NAT & S₁[x,y] )
then reconsider p = x as Polynomial of L by POLYNOM3:def 10;
take y = deg* p; :: thesis: ( y in NAT & S₁[x,y] )
thus ( y in NAT & S₁[x,y] ) by ORDINAL1:def 12; :: thesis: verum

end;

ex f being Function of (Polynom-Ring L),NAT st
for x being object st x in the carrier of (Polynom-Ring L) holds
S₁[x,f . x] from FUNCT_2:sch 1(A);
then consider f being Function of (Polynom-Ring L),NAT such that
H: for x being object st x in the carrier of (Polynom-Ring L) holds
S₁[x,f . x] ;
take f ; :: thesis: for p being Polynomial of L holds f . p = deg* p

now :: thesis: for p being Polynomial of L holds f . p = deg* p

let p be Polynomial of L; :: thesis: f . p = deg* p
p in the carrier of (Polynom-Ring L) by POLYNOM3:def 10;
then S₁[p,f . p] by H;
hence f . p = deg* p ; :: thesis: verum

end;

hence for p being Polynomial of L holds f . p = deg* p ; :: thesis: verum