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] )

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

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:

end;