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 )

now :: thesis: for i being object st i in o1 holds
b1 . 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;

hence b1 = c1 by PBOOLE:3; :: thesis: b2 = c2

now :: thesis: for i being object st i in o2 holds
b2 . 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;

hence b2 = c2 by PBOOLE:3; :: thesis: verum