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