let b be bag of 1; len (divisors b) = (b . 0) + 1
A1:
card (dom (NBag1 | (Segm ((b . 0) + 1)))) = card (rng (NBag1 | (Segm ((b . 0) + 1))))
by CARD_1:70;
(b . 0) + 1 =
card { x where x is bag of 1 : x . 0 <= b . 0 }
by Th14, A1
.=
card (rng (divisors b))
by Th13
.=
card (dom (divisors b))
by CARD_1:70
.=
card (Seg (len (divisors b)))
by FINSEQ_1:def 3
.=
len (divisors b)
;
hence
len (divisors b) = (b . 0) + 1
; verum