theorem Th12: :: BAGORDER:13

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