:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :
for n being Ordinal
for b being bag of n
for b₃ being Nat holds
( b₃ = TotDegree b iff ex f being FinSequence of NAT st
( b₃ = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) );