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

let i be set ; :: thesis: ( i in o1 implies b1 . i = c1 . i )
assume A2: i in o1 ; :: thesis: b1 . i = c1 . i
then reconsider i' = i as Ordinal ;
( (b1 +^ b2) . i' = b1 . i' & (b1 +^ b2) . i' = c1 . i' ) by A1, A2, Def1;
hence b1 . i = c1 . i ; :: thesis: verum

end;

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

now

let i be set ; :: thesis: ( i in o2 implies b2 . i = c2 . i )
assume A3: i in o2 ; :: thesis: b2 . i = c2 . i
then reconsider i' = i as Ordinal ;
A4: o1 +^ i' in o1 +^ o2 by A3, ORDINAL2:49;
o1 c= o1 +^ i' by ORDINAL3:27;
then not o1 +^ i' in o1 by ORDINAL1:7;
then o1 +^ i' in (o1 +^ o2) \ o1 by A4, XBOOLE_0:def 5;
then A5: ( (b1 +^ b2) . (o1 +^ i') = b2 . ((o1 +^ i') -^ o1) & (b1 +^ b2) . (o1 +^ i') = c2 . ((o1 +^ i') -^ o1) ) by A1, Def1;
i' = (o1 +^ i') -^ o1 by ORDINAL3:65;
hence b2 . i = c2 . i by A5; :: thesis: verum

end;

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