let n be Ordinal; :: thesis: decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*>
len <*(EmptyBag n),(EmptyBag n)*> = 2 by FINSEQ_1:44;
then reconsider E = <*(EmptyBag n),(EmptyBag n)*> as Element of 2 -tuples_on (Bags n) by FINSEQ_2:92;
reconsider e = <*E*> as FinSequence of 2 -tuples_on (Bags n) ;
A1: dom e = Seg 1 by FINSEQ_1:38;
A2: <*(EmptyBag n)*> = divisors (EmptyBag n) by Th65;
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:2, TARSKI:def 1;
then A7: (divisors (EmptyBag n)) /. i = EmptyBag n by A2, FINSEQ_4:16;
thus e /. i = E by A6, FINSEQ_4:16
.= <*p,((EmptyBag n) -' p)*> by A5, A7, Th52 ; :: thesis: verum

end;

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