let n be Ordinal; :: thesis: for b being bag of n holds
( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> )
let b be bag of n; :: thesis: ( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> )
reconsider p = (divisors b) /. 1 as bag of n by Def14;
( p = EmptyBag n & 1 in dom (decomp b) ) by Th69, FINSEQ_5:6;
hence (decomp b) /. 1 = <*(EmptyBag n),(b -' (EmptyBag n))*> by Def19
.= <*(EmptyBag n),b*> by Th58 ;
:: thesis: (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*>
reconsider p = (divisors b) /. (len (decomp b)) as bag of n by Def14;
dom (decomp b) = dom (divisors b) by Def19;
then len (decomp b) = len (divisors b) by FINSEQ_3:31;
then A1: p = b by Th69;
len (decomp b) in dom (decomp b) by FINSEQ_5:6;
hence (decomp b) /. (len (decomp b)) = <*b,(b -' b)*> by A1, Def19
.= <*b,(EmptyBag n)*> by Th60 ;
:: thesis: verum