:: deftheorem Def3 defines degree UPROOTS:def 4 :
for A being set
for b being bag of A
for b₃ being Element of NAT holds
( b₃ = degree b iff ex f being FinSequence of NAT st
( b₃ = Sum f & f = b * (canFS (support b)) ) );