Ce qu'a écrit Pseuda est correct : on constitue la suite formellement de façon itérative.
Si cela ne paraît pas "suffisamment rigoureux", c'est qu'on utilise implicitement un théorème de la théorie des ensembles qui affirme l'existence et l'unicité d'une suite définie par une relation de récurrence : en voici l'énoncé dans le cas simple (non paramétré, récurrence simple)
Soit
un ensemble,
et
une fonction dans
.
Alors il existe une unique fonction
telle que
et
[ La démonstration de ce théorème est simple, on distingue existence et unicité, et dans les deux cas on raisonne par l'absurde en utilisant le fait que toute partie de
admet un plus petit élément qui a un prédécesseur s'il n'est pas nul (s'il existe des
pour lesquels la fonction
n'est pas définie, soit le plus petit de ces
, il est plus grand que 0 donc admet un prédécesseur
pour qui la fonction
est définie et par suite la relation donne la valeur de
, contradiciton...) ]
Dans le cas présent,
et
est définie comme
: le théorème précédent affirme l'existence et l'unicité de la suite (reste à justifier que
est bien défini pour tout entier, mais ce n'est pas trop difficile)
Il n'y a plus qu'à vérifier que c'est une bijection entre
et
et ce n'est pas très difficile.
Il n'y a que 10 types de personne au monde : ceux qui comprennent le binaire et ceux qui ne le comprennent pas.