let o1, o2 be Ordinal; :: thesis: for a being Element of Bags o1
for b being Element of Bags o2 st o1 = {} holds
a +^ b = b
let a be Element of Bags o1; :: thesis: for b being Element of Bags o2 st o1 = {} holds
a +^ b = b
let b be Element of Bags o2; :: thesis: ( o1 = {} implies a +^ b = b )
assume A1: o1 = {} ; :: thesis: a +^ b = b
then reconsider ab = a +^ b as Element of Bags o2 by ORDINAL2:47;

now

let i be set ; :: thesis: ( i in o2 implies ab . i = b . i )
assume A2: i in o2 ; :: thesis: ab . i = b . i
then A3: i in (o1 +^ o2) \ o1 by A1, ORDINAL2:47;
reconsider i' = i as Ordinal by A2;
i' -^ o1 = i' by A1, ORDINAL3:69;
hence ab . i = b . i by A3, Def1; :: thesis: verum

end;

hence a +^ b = b by PBOOLE:3; :: thesis: verum