let n be Ordinal; :: thesis: for a, b being bag of n st b divides a holds
TotDegree (a -' b) = (TotDegree a) - (TotDegree b)
let a, b be bag of n; :: thesis: ( b divides a implies TotDegree (a -' b) = (TotDegree a) - (TotDegree b) )
assume b divides a ; :: thesis: TotDegree (a -' b) = (TotDegree a) - (TotDegree b)
then A1: (a -' b) + b = a by PRE_POLY:47;
TotDegree ((a -' b) + b) = (TotDegree (a -' b)) + (TotDegree b) by Th12;
hence TotDegree (a -' b) = (TotDegree a) - (TotDegree b) by A1; :: thesis: verum