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 set st z in dom b1 holds
b1 . z = 0

proof

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

end;

dom b1 = o1 by PARTFUN1:def 4;
then b1 = o1 --> 0 by A2, FUNCOP_1:17;
hence b1 = EmptyBag o1 by POLYNOM1:def 15; :: thesis: b2 = EmptyBag o2
A5: for z being set st z in dom b2 holds
b2 . z = 0

proof

let z be set ; :: thesis: ( z in dom b2 implies b2 . z = 0 )
assume A6: z in dom b2 ; :: thesis: b2 . z = 0
A7: dom b2 = o2 by PARTFUN1:def 4;
then reconsider o = z as Ordinal by A6;
A8: o1 +^ o in o1 +^ o2 by A6, A7, ORDINAL2:49;
o1 c= o1 +^ o by ORDINAL3:27;
then not o1 +^ o in o1 by ORDINAL1:7;
then o1 +^ o in (o1 +^ o2) \ o1 by A8, XBOOLE_0:def 5;
then ( (b1 +^ b2) . (o1 +^ o) = b2 . ((o1 +^ o) -^ o1) & (b1 +^ b2) . (o1 +^ o) = b2 . ((o1 +^ o) -^ o1) ) by Def1;
then b2 . ((o1 +^ o) -^ o1) = 0 by A1, POLYNOM1:56;
hence b2 . z = 0 by ORDINAL3:65; :: thesis: verum

end;

dom b2 = o2 by PARTFUN1:def 4;
then b2 = o2 --> 0 by A5, FUNCOP_1:17;
hence b2 = EmptyBag o2 by POLYNOM1:def 15; :: thesis: verum

end;

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

proof

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

proof

let z be set ; :: thesis: ( z in dom (b1 +^ b2) implies (b1 +^ b2) . z = 0 )
assume A11: z in dom (b1 +^ b2) ; :: thesis: (b1 +^ b2) . z = 0
A12: dom (b1 +^ b2) = o1 +^ o2 by PARTFUN1:def 4;
then reconsider o = z as Ordinal by A11;
( ( o in o1 implies ( b1 . o = 0 & (b1 +^ b2) . o = b1 . o ) ) & ( o in (o1 +^ o2) \ o1 implies ( b2 . (o -^ o1) = 0 & (b1 +^ b2) . o = b2 . (o -^ o1) ) ) ) by A9, Def1, POLYNOM1:56;
hence (b1 +^ b2) . z = 0 by A11, A12, XBOOLE_0:def 5; :: thesis: verum

end;

dom (b1 +^ b2) = o1 +^ o2 by PARTFUN1:def 4;
then b1 +^ b2 = (o1 +^ o2) --> 0 by A10, FUNCOP_1:17;
hence b1 +^ b2 = EmptyBag (o1 +^ o2) by POLYNOM1:def 15; :: thesis: verum

end;