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:30;

now :: thesis: for i being object st i in o2 holds
ab . i = b . i

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

end;

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