let o1, o2 be Ordinal; :: thesis: for a being Element of Bags o1
for b being Element of Bags o2 st o2 = {} holds
a +^ b = a
let a be Element of Bags o1; :: thesis: for b being Element of Bags o2 st o2 = {} holds
a +^ b = a
let b be Element of Bags o2; :: thesis: ( o2 = {} implies a +^ b = a )
assume o2 = {} ; :: thesis: a +^ b = a
then reconsider ab = a +^ b as Element of Bags o1 by ORDINAL2:27;
for i being object st i in o1 holds
ab . i = a . i by Def1;
hence a +^ b = a by PBOOLE:3; :: thesis: verum