あと、定義を満たす集合が二つ（N1,N2)あったとき
N1からN2への全単射写像fがあって

f(N1の0) = N2の0
f(suc(a)) = suc(f(a))

とかを満たす。つまりN1とN2は「同じ」とみなせることも示す必要があるね。
もちろんこれも証明できる。