for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o1 = {} holds
a +^ b = b