let d1, d2 be Nat; :: thesis:

assume p <> 0_ (n,L) ; :: thesis:
given s being bag of n such that A7: s in Support p and
A8: d1 = degree s ; :: thesis:
assume A9: for s1 being bag of n st s1 in Support p holds
d1 >= degree s1 ; :: thesis:
given S being bag of n such that A10: S in Support p and
A11: d2 = degree S ; :: thesis:
assume A12: for s1 being bag of n st s1 in Support p holds
d2 >= degree s1 ; :: thesis:
( d1 <= d2 & d2 <= d1 ) by A7, A8, A9, A10, A11, A12;
hence d1 = d2 by XXREAL_0:1; :: thesis:

end;

hence ( ( p <> 0_ (n,L) & ex s being bag of n st
( s in Support p & d1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= d1 ) & ex s being bag of n st
( s in Support p & d2 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= d2 ) implies d1 = d2 ) & ( not p <> 0_ (n,L) & d1 = 0 & d2 = 0 implies d1 = d2 ) ) ; :: thesis: