let X be set ; :: thesis: for b being bag of holds b / b = EmptyBag X
let b be bag of ; :: thesis: b / b = EmptyBag X
b + (EmptyBag X) = b by POLYNOM1:57;
hence b / b = EmptyBag X by Def1; :: thesis: verum