thus
( p <> 0_ (n,L) implies ex d being Nat st

( ex s being bag of n st

( s in Support p & d = degree s ) & ( for s1 being bag of n st s1 in Support p holds

d >= degree s1 ) ) ) :: thesis: ( not p <> 0_ (n,L) implies ex b_{1} being Nat st b_{1} = 0 )_{1} being Nat st b_{1} = 0 )
; :: thesis: verum

( ex s being bag of n st

( s in Support p & d = degree s ) & ( for s1 being bag of n st s1 in Support p holds

d >= degree s1 ) ) ) :: thesis: ( not p <> 0_ (n,L) implies ex b

proof

thus
( not p <> 0_ (n,L) implies ex b
assume
p <> 0_ (n,L)
; :: thesis: ex d being Nat st

( ex s being bag of n st

( s in Support p & d = degree s ) & ( for s1 being bag of n st s1 in Support p holds

d >= degree s1 ) )

then p <> (dom p) --> (0. L) ;

then consider b being object such that

A1: ( b in dom p & p . b <> 0. L ) by FUNCOP_1:11;

reconsider b = b as bag of n by A1;

defpred S_{1}[ object , object ] means for s being bag of n st s = $1 holds

$2 = degree s;

A2: for e being object st e in Support p holds

ex u being object st S_{1}[e,u]

A3: ( dom D = Support p & ( for e being object st e in Support p holds

S_{1}[e,D . e] ) )
from CLASSES1:sch 1(A2);

b in Support p by A1, POLYNOM1:def 3;

then dom D <> {} by A3, XBOOLE_0:def 1;

then A4: rng D <> {} by RELAT_1:42;

max R in R by XXREAL_2:def 8;

then consider s being object such that

A6: ( s in dom D & max R = D . s ) by FUNCT_1:def 3;

reconsider s = s as bag of n by A6, A3;

reconsider m = max R as Nat by A6;

take m ; :: thesis: ( ex s being bag of n st

( s in Support p & m = degree s ) & ( for s1 being bag of n st s1 in Support p holds

m >= degree s1 ) )

( s in Support p & m = degree s ) by A6, A3;

hence ex s being bag of n st

( s in Support p & m = degree s ) ; :: thesis: for s1 being bag of n st s1 in Support p holds

m >= degree s1

let s1 be bag of n; :: thesis: ( s1 in Support p implies m >= degree s1 )

assume s1 in Support p ; :: thesis: m >= degree s1

then ( D . s1 in R & D . s1 = degree s1 ) by FUNCT_1:def 3, A3;

hence m >= degree s1 by XXREAL_2:def 8; :: thesis: verum

end;( ex s being bag of n st

( s in Support p & d = degree s ) & ( for s1 being bag of n st s1 in Support p holds

d >= degree s1 ) )

then p <> (dom p) --> (0. L) ;

then consider b being object such that

A1: ( b in dom p & p . b <> 0. L ) by FUNCOP_1:11;

reconsider b = b as bag of n by A1;

defpred S

$2 = degree s;

A2: for e being object st e in Support p holds

ex u being object st S

proof

consider D being Function such that
let e be object ; :: thesis: ( e in Support p implies ex u being object st S_{1}[e,u] )

assume e in Support p ; :: thesis: ex u being object st S_{1}[e,u]

then reconsider e = e as bag of n ;

take degree e ; :: thesis: S_{1}[e, degree e]

thus S_{1}[e, degree e]
; :: thesis: verum

end;assume e in Support p ; :: thesis: ex u being object st S

then reconsider e = e as bag of n ;

take degree e ; :: thesis: S

thus S

A3: ( dom D = Support p & ( for e being object st e in Support p holds

S

b in Support p by A1, POLYNOM1:def 3;

then dom D <> {} by A3, XBOOLE_0:def 1;

then A4: rng D <> {} by RELAT_1:42;

now :: thesis: for y being object st y in rng D holds

y is natural

then reconsider R = rng D as non empty finite natural-membered set by A4, A3, FINSET_1:8, MEMBERED:def 6;y is natural

let y be object ; :: thesis: ( y in rng D implies y is natural )

assume y in rng D ; :: thesis: y is natural

then consider x being object such that

A5: ( x in dom D & y = D . x ) by FUNCT_1:def 3;

reconsider x = x as bag of n by A5, A3;

y = degree x by A5, A3;

hence y is natural ; :: thesis: verum

end;assume y in rng D ; :: thesis: y is natural

then consider x being object such that

A5: ( x in dom D & y = D . x ) by FUNCT_1:def 3;

reconsider x = x as bag of n by A5, A3;

y = degree x by A5, A3;

hence y is natural ; :: thesis: verum

max R in R by XXREAL_2:def 8;

then consider s being object such that

A6: ( s in dom D & max R = D . s ) by FUNCT_1:def 3;

reconsider s = s as bag of n by A6, A3;

reconsider m = max R as Nat by A6;

take m ; :: thesis: ( ex s being bag of n st

( s in Support p & m = degree s ) & ( for s1 being bag of n st s1 in Support p holds

m >= degree s1 ) )

( s in Support p & m = degree s ) by A6, A3;

hence ex s being bag of n st

( s in Support p & m = degree s ) ; :: thesis: for s1 being bag of n st s1 in Support p holds

m >= degree s1

let s1 be bag of n; :: thesis: ( s1 in Support p implies m >= degree s1 )

assume s1 in Support p ; :: thesis: m >= degree s1

then ( D . s1 in R & D . s1 = degree s1 ) by FUNCT_1:def 3, A3;

hence m >= degree s1 by XXREAL_2:def 8; :: thesis: verum