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