for n being Ordinal
for a, b being bag of n holds TotDegree (a + b) = (TotDegree a) + (TotDegree b)