let n be Ordinal; :: thesis: decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*>
len <*(EmptyBag n),(EmptyBag n)*> = 2 by FINSEQ_1:61;
then reconsider E = <*(EmptyBag n),(EmptyBag n)*> as Element of 2 -tuples_on (Bags n) by FINSEQ_2:110;
reconsider e = <*E*> as FinSequence of 2 -tuples_on (Bags n) ;
A1: dom e = Seg 1 by FINSEQ_1:55;
A2: <*(EmptyBag n)*> = divisors (EmptyBag n) by Th71;
A3: for i being Element of NAT
for p being bag of n st i in dom e & p = (divisors (EmptyBag n)) /. i holds
e /. i = <*p,((EmptyBag n) -' p)*>

proof

let i be Element of NAT ; :: thesis: for p being bag of n st i in dom e & p = (divisors (EmptyBag n)) /. i holds
e /. i = <*p,((EmptyBag n) -' p)*>
let p be bag of n; :: thesis: ( i in dom e & p = (divisors (EmptyBag n)) /. i implies e /. i = <*p,((EmptyBag n) -' p)*> )
assume that
A4: i in dom e and
A5: p = (divisors (EmptyBag n)) /. i ; :: thesis: e /. i = <*p,((EmptyBag n) -' p)*>
A6: i = 1 by A1, A4, FINSEQ_1:4, TARSKI:def 1;
then A7: (divisors (EmptyBag n)) /. i = EmptyBag n by A2, FINSEQ_4:25;
thus e /. i = E by A6, FINSEQ_4:25
.= <*p,((EmptyBag n) -' p)*> by A5, A7, Th58 ; :: thesis: verum

end;

dom e = dom (divisors (EmptyBag n)) by A2, A1, FINSEQ_1:55;
hence decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*> by A3, Def19; :: thesis: verum