let b be bag of ; :: thesis: decomp b = <*<*{} ,{} *>*>
b in Bags {} by POLYNOM1:def 14;
then A1: b = {} by POLYNOM1:55, TARSKI:def 1;
A2: EmptyBag {} = {} --> 0 by POLYNOM1:def 15;
then divisors b = <*{} *> by A1, POLYNOM1:71;
then A3: len (divisors b) = 1 by FINSEQ_1:56;
A4: dom (divisors b) = dom (decomp b) by POLYNOM1:def 19;
then A5: len (decomp b) = 1 by A3, FINSEQ_3:31;
1 in dom (decomp b) by A3, A4, FINSEQ_3:27;
then (decomp b) . 1 = (decomp b) /. 1 by PARTFUN1:def 8
.= <*{} ,{} *> by A1, A2, POLYNOM1:75 ;
hence decomp b = <*<*{} ,{} *>*> by A5, FINSEQ_1:57; :: thesis: verum