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;
rng <*E*> c= 2 -tuples_on (Bags n)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng <*E*> or u in 2 -tuples_on (Bags n) )
assume u in rng <*E*> ; :: thesis: u in 2 -tuples_on (Bags n)
then u in {E} by FINSEQ_1:56;
then u = E by TARSKI:def 1;
hence u in 2 -tuples_on (Bags n) ; :: thesis: verum

end;

then reconsider e = <*E*> as FinSequence of 2 -tuples_on (Bags n) by FINSEQ_1:def 4;
A1: <*(EmptyBag n)*> = divisors (EmptyBag n) by Th71;
A2: dom e = Seg 1 by FINSEQ_1:55;
then A3: dom e = dom (divisors (EmptyBag n)) by A1, FINSEQ_1:55;
for i being Element of NAT
for p being bag of 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 st i in dom e & p = (divisors (EmptyBag n)) /. i holds
e /. i = <*p,((EmptyBag n) -' p)*>
let p be bag of ; :: 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 A2, A4, FINSEQ_1:4, TARSKI:def 1;
then A7: (divisors (EmptyBag n)) /. i = EmptyBag n by A1, FINSEQ_4:25;
thus e /. i = E by A6, FINSEQ_4:25
.= <*p,((EmptyBag n) -' p)*> by A5, A7, Th58 ; :: thesis: verum

end;

hence decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*> by A3, Def19; :: thesis: verum