Binary Kraft criterion for finite positive codeword lengths

If a prefix code has lengths ${\mathrm{\ell }}_i$, its finite set of codewords is prefix-free by [F3]. Apply the first assertion of [F1] to that set; the codewords are distinct by nonsingularity, so its Kraft sum is exactly ${\sum }_i{2}^{-{\mathrm{\ell }}_i}\le 1$.

Suppose ${\sum }_i{2}^{-{\mathrm{\ell }}_i}\le 1$. Enumerate the finite request list $(i,{\mathrm{\ell }}_i)$ in increasing order of $i$; this is a computable enumeration, and the requested lengths are positive by hypothesis. The converse in [F1] allocates distinct prefix-free binary words of those lengths. Assign the word allocated to request $i$ as $C(i)$. Their positive lengths make $C$ a binary source code by [F2]. Distinctness gives nonsingularity and prefix-freeness gives [F3], so the requested binary prefix code exists.