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;

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

hence
a +^ b = b
by PBOOLE:3; :: thesis: verumab . 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;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