let d1, d2 be Nat; :: thesis: ( ( 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 ) )

( 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: verum

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

now :: thesis: ( 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

d1 >= degree s1 ) & 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

d2 >= degree s1 ) implies d1 = d2 )

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

d1 >= degree s1 ) & 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

d2 >= degree s1 ) implies d1 = d2 )

assume
p <> 0_ (n,L)
; :: thesis: ( 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

d1 >= degree s1 ) & 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

d2 >= degree s1 ) implies d1 = d2 )

given s being bag of n such that A7: s in Support p and

A8: d1 = degree s ; :: thesis: ( ( for s1 being bag of n st s1 in Support p holds

d1 >= degree s1 ) & 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

d2 >= degree s1 ) implies d1 = d2 )

assume A9: for s1 being bag of n st s1 in Support p holds

d1 >= degree s1 ; :: thesis: ( 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

d2 >= degree s1 ) implies d1 = d2 )

given S being bag of n such that A10: S in Support p and

A11: d2 = degree S ; :: thesis: ( ( for s1 being bag of n st s1 in Support p holds

d2 >= degree s1 ) implies d1 = d2 )

assume A12: for s1 being bag of n st s1 in Support p holds

d2 >= degree s1 ; :: thesis: d1 = d2

( d1 <= d2 & d2 <= d1 ) by A7, A8, A9, A10, A11, A12;

hence d1 = d2 by XXREAL_0:1; :: thesis: verum

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

d1 >= degree s1 ) & 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

d2 >= degree s1 ) implies d1 = d2 )

given s being bag of n such that A7: s in Support p and

A8: d1 = degree s ; :: thesis: ( ( for s1 being bag of n st s1 in Support p holds

d1 >= degree s1 ) & 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

d2 >= degree s1 ) implies d1 = d2 )

assume A9: for s1 being bag of n st s1 in Support p holds

d1 >= degree s1 ; :: thesis: ( 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

d2 >= degree s1 ) implies d1 = d2 )

given S being bag of n such that A10: S in Support p and

A11: d2 = degree S ; :: thesis: ( ( for s1 being bag of n st s1 in Support p holds

d2 >= degree s1 ) implies d1 = d2 )

assume A12: for s1 being bag of n st s1 in Support p holds

d2 >= degree s1 ; :: thesis: d1 = d2

( d1 <= d2 & d2 <= d1 ) by A7, A8, A9, A10, A11, A12;

hence d1 = d2 by XXREAL_0:1; :: thesis: verum

( 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: verum