>>7
厳密性を追求するなら、それだけでは全くダメだよ。

>>1にはしれっと「有限数の要素を持つ集合」と書いてあるが、
まず有限集合とは何かという定義が必要。

もちろん、ある非負整数nが存在して、[0,n)からAへの全単射が存在するときに
「有限集合」と呼ぶわけだ(別の流儀もあるが、ここでは使わない)。
そして、このnのことを、>>1ではn(A)と書いているわけだ。

しかし、このときのnすなわちn(A)がAごとに「一意的に決まること」をまず証明しなければならない。
これが自明に見えて意外と面倒くさい。これを示すには、n＜mのときに[0,n)から[0,m)への全単射が
存在しないことを言えばいいのだが、まさにそれが面倒くさい。直観的には、[0,n)よりも[0,m)の方が
要素の個数が多いのだから、全単射が存在しないのは明らかに見えるが、今まさに「個数」に相当する概念の
一意性を証明しようとしているのだから、「個数」の直観に基づいたあやふやな議論は排除しなければならない。
そんなこと言ったって、[0,m)側はいくつかの要素が明らかに余るだろうと思うだろうが、要素が余るという性質を
いかにして n＜m という不等式から導くかがポイントになるのであり、やはり全く自明ではないのだ。
で、これが証明できたとして、まだ面倒くさいのが残っていて、それは次の定理だ。

定理：Aが有限集合でB⊂Aならば、Bも有限集合である。

これは、「有限集合」の定義の仕方によって証明の面倒くささが変わる。
今回の定義の仕方だと、面倒くさい部類になる。ここまで証明できて初めて
>>1のスタートラインに立てて、そのあとは>>3,>>4と大差ない議論になる。