for o1, o2 being Ordinal
for a1, b1, c1 being Element of Bags o1
for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2