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

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