let o1, o2 be Ordinal; :: thesis: for b1 being Element of Bags o1
for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )
let b1 be Element of Bags o1; :: thesis: for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )
let b2 be Element of Bags o2; :: thesis: ( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )

hereby :: thesis: ( b1 = EmptyBag o1 & b2 = EmptyBag o2 implies b1 +^ b2 = EmptyBag (o1 +^ o2) )

assume A1: b1 +^ b2 = EmptyBag (o1 +^ o2) ; :: thesis: ( b1 = EmptyBag o1 & b2 = EmptyBag o2 )
A2: for z being object st z in dom b1 holds
b1 . z = 0

proof

let z be object ; :: thesis: ( z in dom b1 implies b1 . z = 0 )
A3: dom b1 = o1 by PARTFUN1:def 2;
assume A4: z in dom b1 ; :: thesis: b1 . z = 0
then reconsider o = z as Ordinal by A3;
b1 . o = (b1 +^ b2) . o by A4, A3, Def1
.= 0 by A1, PBOOLE:5 ;
hence b1 . z = 0 ; :: thesis: verum

end;

dom b1 = o1 by PARTFUN1:def 2;
then b1 = o1 --> 0 by A2, FUNCOP_1:11;
hence b1 = EmptyBag o1 by PBOOLE:def 3; :: thesis: b2 = EmptyBag o2
A5: for z being object st z in dom b2 holds
b2 . z = 0

proof

let z be object ; :: thesis: ( z in dom b2 implies b2 . z = 0 )
A6: dom b2 = o2 by PARTFUN1:def 2;
assume A7: z in dom b2 ; :: thesis: b2 . z = 0
then reconsider o = z as Ordinal by A6;
o1 c= o1 +^ o by ORDINAL3:24;
then A8: not o1 +^ o in o1 by ORDINAL1:5;
o1 +^ o in o1 +^ o2 by A7, A6, ORDINAL2:32;
then o1 +^ o in (o1 +^ o2) \ o1 by A8, XBOOLE_0:def 5;
then (b1 +^ b2) . (o1 +^ o) = b2 . ((o1 +^ o) -^ o1) by Def1;
then b2 . ((o1 +^ o) -^ o1) = 0 by A1, PBOOLE:5;
hence b2 . z = 0 by ORDINAL3:52; :: thesis: verum

end;

dom b2 = o2 by PARTFUN1:def 2;
then b2 = o2 --> 0 by A5, FUNCOP_1:11;
hence b2 = EmptyBag o2 by PBOOLE:def 3; :: thesis: verum

end;

thus ( b1 = EmptyBag o1 & b2 = EmptyBag o2 implies b1 +^ b2 = EmptyBag (o1 +^ o2) ) :: thesis: verum

proof

assume that
A9: b1 = EmptyBag o1 and
A10: b2 = EmptyBag o2 ; :: thesis: b1 +^ b2 = EmptyBag (o1 +^ o2)
A11: for z being object st z in dom (b1 +^ b2) holds
(b1 +^ b2) . z = 0

proof

let z be object ; :: thesis: ( z in dom (b1 +^ b2) implies (b1 +^ b2) . z = 0 )
A12: dom (b1 +^ b2) = o1 +^ o2 by PARTFUN1:def 2;
assume A13: z in dom (b1 +^ b2) ; :: thesis: (b1 +^ b2) . z = 0
then reconsider o = z as Ordinal by A12;
A14: ( o in (o1 +^ o2) \ o1 implies ( b2 . (o -^ o1) = 0 & (b1 +^ b2) . o = b2 . (o -^ o1) ) ) by A10, Def1, PBOOLE:5;
( o in o1 implies ( b1 . o = 0 & (b1 +^ b2) . o = b1 . o ) ) by A9, Def1, PBOOLE:5;
hence (b1 +^ b2) . z = 0 by A13, A12, A14, XBOOLE_0:def 5; :: thesis: verum

end;

dom (b1 +^ b2) = o1 +^ o2 by PARTFUN1:def 2;
then b1 +^ b2 = (o1 +^ o2) --> 0 by A11, FUNCOP_1:11;
hence b1 +^ b2 = EmptyBag (o1 +^ o2) by PBOOLE:def 3; :: thesis: verum

end;