theorem Th20: :: POLYNOM9:20

for X being set
for b1, b2 being bag of X st (2 (#) b1) +* (0,(b1 . 0)) = (2 (#) b2) +* (0,(b2 . 0)) holds
b1 = b2