A1: dom (divisors b) = dom (decomp b) by Def19;
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 such that
A4: (decomp b) /. m = <*bm1,bm2*> and
b = bm1 + bm2 by Th72;
assume (decomp b) /. k = (decomp b) /. m ; :: thesis: k = m
then (divisors b) /. k = bm1 by A2, A4, Th74
.= (divisors b) /. m by A3, A4, Th74 ;
hence k = m by A1, A2, A3, PARTFUN2:17; :: thesis: verum

end;

hence decomp b is one-to-one by PARTFUN2:16; :: thesis: decomp b is FinSequence-yielding
let x be set ; :: according to MATRLIN:def 1 :: thesis: ( not x in dom (decomp b) or (decomp b) . x is set )
assume A5: x in dom (decomp b) ; :: thesis: (decomp b) . x is set
then reconsider k = x as Element of NAT ;
reconsider p = (divisors b) /. k as bag of by Def14;
(decomp b) /. k = <*p,(b -' p)*> by A5, Def19;
hence (decomp b) . x is set by A5, PARTFUN1:def 8; :: thesis: verum