let b be bag of 0 ; :: thesis: decomp b = <*<*{},{}*>*>
b in Bags {} by PRE_POLY:def 12;
then A1: b = {} by PRE_POLY:51, TARSKI:def 1;
A2: EmptyBag {} = {} --> 0 by PRE_POLY:def 13;
then divisors b = <*{}*> by A1, PRE_POLY:67;
then A3: len (divisors b) = 1 by FINSEQ_1:39;
A4: dom (divisors b) = dom (decomp b) by PRE_POLY:def 17;
then 1 in dom (decomp b) by A3, FINSEQ_3:25;
then A5: (decomp b) . 1 = (decomp b) /. 1 by PARTFUN1:def 6
.= <*{},{}*> by A1, A2, PRE_POLY:71 ;
len (decomp b) = 1 by A3, A4, FINSEQ_3:29;
hence decomp b = <*<*{},{}*>*> by A5, FINSEQ_1:40; :: thesis: verum