theorem :: GLIB_004:7

for A1, A2 being set
for b1 being Rbag of A1
for b2 being Rbag of A2 st b1 = b2 holds
Sum b1 = Sum b2