theorem Th4: :: GLIB_004:4

for X, x being set
for b being Rbag of X st dom b = {x} holds
Sum b = b . x