theorem Th8: :: GLIB_004:8

for X, x being set
for b being Rbag of X
for y being Real st b = (EmptyBag X) +* (x .--> y) holds
Sum b = y