A1: dom (divisors b) = dom (decomp b) by Def17;
hence not decomp b is empty ; :: thesis: ( decomp b is one-to-one & decomp b is FinSequence-yielding )

now

let k, m be Element of NAT ; :: thesis: ( k in dom (decomp b) & m in dom (decomp b) & (decomp b) /. k = (decomp b) /. m implies k = m )
assume A2: k in dom (decomp b) ; :: thesis: ( m in dom (decomp b) & (decomp b) /. k = (decomp b) /. m implies k = m )
assume A3: m in dom (decomp b) ; :: thesis: ( (decomp b) /. k = (decomp b) /. m implies k = m )
then consider bm1, bm2 being bag of n such that
A4: (decomp b) /. m = <*bm1,bm2*> and
b = bm1 + bm2 by Th68;
assume (decomp b) /. k = (decomp b) /. m ; :: thesis: k = m
then (divisors b) /. k = bm1 by A2, A4, Th70
.= (divisors b) /. m by A3, A4, Th70 ;
hence k = m by A1, A2, A3, PARTFUN2:10; :: thesis: verum

end;

hence decomp b is one-to-one by PARTFUN2:9; :: thesis: decomp b is FinSequence-yielding
let x be set ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom (decomp b) implies (decomp b) . x is FinSequence )
assume A5: x in dom (decomp b) ; :: thesis: (decomp b) . x is FinSequence
then reconsider k = x as Element of NAT ;
reconsider p = (divisors b) /. k as bag of n ;
(decomp b) /. k = <*p,(b -' p)*> by A5, Def17;
hence (decomp b) . x is FinSequence by A5, PARTFUN1:def 6; :: thesis: verum