let o1, o2 be Ordinal; :: thesis: for b1, c1 being Element of Bags o1

for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds

( b1 = c1 & b2 = c2 )

let b1, c1 be Element of Bags o1; :: thesis: for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds

( b1 = c1 & b2 = c2 )

let b2, c2 be Element of Bags o2; :: thesis: ( b1 +^ b2 = c1 +^ c2 implies ( b1 = c1 & b2 = c2 ) )

assume A1: b1 +^ b2 = c1 +^ c2 ; :: thesis: ( b1 = c1 & b2 = c2 )

for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds

( b1 = c1 & b2 = c2 )

let b1, c1 be Element of Bags o1; :: thesis: for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds

( b1 = c1 & b2 = c2 )

let b2, c2 be Element of Bags o2; :: thesis: ( b1 +^ b2 = c1 +^ c2 implies ( b1 = c1 & b2 = c2 ) )

assume A1: b1 +^ b2 = c1 +^ c2 ; :: thesis: ( b1 = c1 & b2 = c2 )

now :: thesis: for i being object st i in o1 holds

b1 . i = c1 . i

hence
b1 = c1
by PBOOLE:3; :: thesis: b2 = c2b1 . i = c1 . i

let i be object ; :: thesis: ( i in o1 implies b1 . i = c1 . i )

assume A2: i in o1 ; :: thesis: b1 . i = c1 . i

then reconsider i9 = i as Ordinal ;

(b1 +^ b2) . i9 = b1 . i9 by A2, Def1;

hence b1 . i = c1 . i by A1, A2, Def1; :: thesis: verum

end;assume A2: i in o1 ; :: thesis: b1 . i = c1 . i

then reconsider i9 = i as Ordinal ;

(b1 +^ b2) . i9 = b1 . i9 by A2, Def1;

hence b1 . i = c1 . i by A1, A2, Def1; :: thesis: verum

now :: thesis: for i being object st i in o2 holds

b2 . i = c2 . i

hence
b2 = c2
by PBOOLE:3; :: thesis: verumb2 . i = c2 . i

let i be object ; :: thesis: ( i in o2 implies b2 . i = c2 . i )

assume A3: i in o2 ; :: thesis: b2 . i = c2 . i

then reconsider i9 = i as Ordinal ;

A4: i9 = (o1 +^ i9) -^ o1 by ORDINAL3:52;

o1 c= o1 +^ i9 by ORDINAL3:24;

then A5: not o1 +^ i9 in o1 by ORDINAL1:5;

o1 +^ i9 in o1 +^ o2 by A3, ORDINAL2:32;

then A6: o1 +^ i9 in (o1 +^ o2) \ o1 by A5, XBOOLE_0:def 5;

then (b1 +^ b2) . (o1 +^ i9) = b2 . ((o1 +^ i9) -^ o1) by Def1;

hence b2 . i = c2 . i by A1, A6, A4, Def1; :: thesis: verum

end;assume A3: i in o2 ; :: thesis: b2 . i = c2 . i

then reconsider i9 = i as Ordinal ;

A4: i9 = (o1 +^ i9) -^ o1 by ORDINAL3:52;

o1 c= o1 +^ i9 by ORDINAL3:24;

then A5: not o1 +^ i9 in o1 by ORDINAL1:5;

o1 +^ i9 in o1 +^ o2 by A3, ORDINAL2:32;

then A6: o1 +^ i9 in (o1 +^ o2) \ o1 by A5, XBOOLE_0:def 5;

then (b1 +^ b2) . (o1 +^ i9) = b2 . ((o1 +^ i9) -^ o1) by Def1;

hence b2 . i = c2 . i by A1, A6, A4, Def1; :: thesis: verum