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₁ being Nat st b₁ = 0 )

proof

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₁[ 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₁[e,u]

proof

let e be object ; :: thesis: ( e in Support p implies ex u being object st S₁[e,u] )
assume e in Support p ; :: thesis: ex u being object st S₁[e,u]
then reconsider e = e as bag of n ;
take degree e ; :: thesis: S₁[e, degree e]
thus S₁[e, degree e] ; :: thesis: verum

end;

consider D being Function such that
A3: ( dom D = Support p & ( for e being object st e in Support p holds
S₁[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;

now :: thesis: for y being object st y in rng D holds
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;

then reconsider R = rng D as non empty finite natural-membered set by A4, A3, FINSET_1:8, MEMBERED:def 6;
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;

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