A1:
dom (divisors b) = dom (decomp b)
by Def16;
hence
not decomp b is empty
; ( decomp b is one-to-one & decomp b is FinSequence-yielding )
now 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 = mlet k,
m be
Element of
NAT ;
( 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)
;
( m in dom (decomp b) & (decomp b) /. k = (decomp b) /. m implies k = m )assume A3:
m in dom (decomp b)
;
( (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
;
k = mthen (divisors b) /. k =
bm1
by A2, A4, Th68
.=
(divisors b) /. m
by A3, A4, Th68
;
hence
k = m
by A1, A2, A3, PARTFUN2:10;
verum end;
hence
decomp b is one-to-one
by PARTFUN2:9; decomp b is FinSequence-yielding
let x be object ; PRE_POLY:def 3 ( x in dom (decomp b) implies (decomp b) . x is FinSequence )
assume
x in dom (decomp b)
; (decomp b) . x is FinSequence
thus
(decomp b) . x is FinSequence
; verum