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

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