for A being set
for b1, b2 being Rbag of A st ( for x being set st x in A holds
b1 . x = b2 . x ) holds
Sum b1 = Sum b2