Big-endian bit-string indices are bijective

At $n=0$, the domain has just the empty word and the codomain is $\{0,\dots ,2^0-1\}=\{0\}$. By [F1], its index is $0$, so the map is bijective.

Assume the result for $n$. For a word of length $n+1$, write its first bit as $b\in \{0,1\}$ and its remaining word as $y\in \{0,1{\}}^n$. Splitting the first term from the sum in [F1] gives ${\mathrm{enc}}_{n+1}(b,y)=b{2}^n+{\mathrm{enc}}_n(y)$. By the induction hypothesis, the tail index ranges bijectively over $\{0,\dots ,2^n-1\}$.

If $b=0$, the resulting indices are exactly $0,\dots ,2^n-1$. If $b=1$, they are exactly $2^n,\dots ,2^{n+1}-1$. The two intervals are disjoint and their union is the full target, so equality of two encoded indices forces the first bits to agree and every target index is attained. For either fixed first bit, injectivity and surjectivity of the tail encoding give the corresponding claims for the remaining word.

By [F5], the base case and induction step prove bijectivity for all $n\ge 0$. A permutation $\sigma$ of the bit positions is a bijection on words, with inverse the permutation ${\sigma }^{-1}$; composing it with the basis labeling in [F2] therefore permutes the basis [F3, F4].