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 ;
( p = EmptyBag n & 1 in dom (decomp b) ) by Th63, FINSEQ_5:6;
hence (decomp b) /. 1 = <*(EmptyBag n),(b -' (EmptyBag n))*> by Def16
.= <*(EmptyBag n),b*> by Th52 ;
:: thesis: (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*>
reconsider p = (divisors b) /. (len (decomp b)) as bag of n ;
dom (decomp b) = dom (divisors b) by Def16;
then len (decomp b) = len (divisors b) by FINSEQ_3:29;
then A1: p = b by Th63;
len (decomp b) in dom (decomp b) by FINSEQ_5:6;
hence (decomp b) /. (len (decomp b)) = <*b,(b -' b)*> by A1, Def16
.= <*b,(EmptyBag n)*> by Th54 ;
:: thesis: verum