Nice problem! I have a solution that uses my beloved Axiom of Choice Let us define the equivalence relation between positive real numbers: "$a \equiv b$ if $a-b$ has only finitely non-zero digits". It is reflexive (a-a = 0 that doesn't have non-zero digits), symmetric (a-b = -(b-a) and they have the same digits) and transitive ( $(a-b)+(b-c) = (a-c)$ and the sum of two numbers of the form $\frac{n}{10^{k}}$ is of this form). So, this equivalence relations partitions the set of positive reals in a family of disjoint sets (classes of equivalence). Let $f(a)$ be the equivalence class containing a. Let $g$ be a choice function of the equivalence classes (and here we use AC). Now we finally define $c: \mathbb{R}^{+}\rightarrow \mathbb{Z}_{10}$ such that c(r) is the sum of the decimal digits (mod 10) of $a-g(f(a))$. In fact, $a \equiv g(f(a))$, so their difference has just a finite number of nonzero digits, and we can calculate this sum. If two numbers a,b differ only in one place of their decimal rappresentation, $c(a)-c(b)$ is the sum of the decimal digits of their difference, that by hypotesis has one and only one nonzero digit $\Rightarrow c(a) \neq c(b)$. Is it clear? Now I ask you either to prove this problem without the Axiom of Choice, or to prove (a weak form of) the Axiom of Choice using this problem