let n be Ordinal; 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 ;
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;
( 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
;
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
;
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; verum