A1: dom (divisors b) = dom (decomp b) by Def16;
hence not decomp b is empty ; :: thesis: ( decomp b is one-to-one & decomp b is FinSequence-yielding )
now :: thesis: for k, m being Element of NAT st k in dom (decomp b) & m in dom (decomp b) & (decomp b) /. k = (decomp b) /. m holds
k = m
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 Th66;
assume (decomp b) /. k = (decomp b) /. m ; :: thesis: k = m
then (divisors b) /. k = bm1 by A2, A4, Th68
.= (divisors b) /. m by A3, A4, Th68 ;
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 object ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom (decomp b) implies (decomp b) . x is FinSequence )
assume x in dom (decomp b) ; :: thesis: (decomp b) . x is FinSequence
thus (decomp b) . x is FinSequence ; :: thesis: verum