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