let X be set ; :: thesis: for b1, b2 being bag of holds (b1 + b2) / b2 = b1
let b1, b2 be bag of ; :: thesis: (b1 + b2) / b2 = b1
b2 divides b1 + b2 by POLYNOM1:54;
then b2 + ((b1 + b2) / b2) = b1 + b2 by GROEB_2:def 1;
then (b2 + ((b1 + b2) / b2)) -' b2 = b1 by POLYNOM1:52;
hence (b1 + b2) / b2 = b1 by POLYNOM1:52; :: thesis: verum