let n be Ordinal; :: thesis: for a, b being bag of st b divides a holds
TotDegree (a -' b) = (TotDegree a) - (TotDegree b)
let a, b be bag of ; :: 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 POLYNOM1:51;
TotDegree ((a -' b) + b) = (TotDegree (a -' b)) + (TotDegree b) by Th14;
hence TotDegree (a -' b) = (TotDegree a) - (TotDegree b) by A1; :: thesis: verum