Define an injective map \(f: \mathbb{Z}_+ \to X^\omega\), where \(X\) is the two-element set \(\{0, 1\}\), without using the choice axiom.
Solution
For \(n\in\mathbb Z_+\), define \[ f(n)=(\underbrace{1,\ldots,1}_{n\text{ entries}},0,0,\ldots)\in X^\omega. \] If \(m<n\), then the \(n\)-th coordinate of \(f(m)\) is \(0\), whereas the \(n\)-th coordinate of \(f(n)\) is \(1\). Hence \(f(m)\ne f(n)\), so \(f\) is injective.
The construction is explicit and makes no choices from an arbitrary family of sets, so no form of the axiom of choice is used.