\(k\) 個の元の集合から \(n\) 個の元の集合への単射は \(n!/(n-k)!\) 個。階乗は割らずに、\(m \cdot (n-k)! = n!\) の形で述べる。
1点を除いた集合・1点を足した集合の所属（Ln・Lu）。
Ln … \(x \notin X \mathop\setminus \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
Lu … \(x \in X \cup \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1 準備

単射 \(f\) とは、写像で、異なる \(p, q\) が同じ値 \(y\) に行かないもの（\(\langle p, y\rangle \in f\) かつ \(\langle q, y\rangle \in f\) なら \(p = q\)）。

1.1 1点を除く

\(z \in X\) の像が \(a\) である単射の全体 \(F\) は、\(X \setminus \{z\}\) から \(Y \setminus \{a\}\) への単射の全体 \(G\) と同じ個数（LFib の単射版）。
LFibI … \(z \in X , a \in Y , \forall f \, ( f \in F \Longleftrightarrow f \in X \to Y , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) , \langle z , a \rangle \in f ) , \forall g \, ( g \in G \Longleftrightarrow g \in X \mathop\setminus \{ z \} \to Y \mathop\setminus \{ a \} , \forall p , q , y \, ( \langle p , y \rangle \in g , \langle q , y \rangle \in g \Longrightarrow p = q ) ) \Longrightarrow F \stackrel{\#}= G\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，Ln ，∈∖1

1.2 単射の集合が在ること

集合 \(X, Y\) について、\(X\) から \(Y\) への単射の全体は集合（\(X \times Y\) の部分集合の部分集合）。
Lex … \(\exists G \, \forall g \, ( g \in G \Longleftrightarrow g \in X \to Y , \forall p , q , y \, ( \langle p , y \rangle \in g , \langle q , y \rangle \in g \Longrightarrow p = q ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
階乗は 0 でない。
L!ℕ … \(n \in \mathbb{M} \Longrightarrow n ! \in \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄

1.3 ファイバーの和

\(k\) 個から \(k + j\) 個への単射が \(q\) 個なら、\(k + 1\) 個から \((k + j) + 1\) 個への単射は \(q \cdot ((k + j) + 1)\) 個（\(z\) の行き先 \(a\) ごとに分ける）。
LIN … \(k , j \in \mathbb{M} , q \in \mathbb{M} , \forall U , V , G \, ( U \stackrel{\#}= k , V \stackrel{\#}= k + j , \forall f \, ( f \in G \Longleftrightarrow f \in U \to V , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow G \stackrel{\#}= q ) , X \stackrel{\#}= k + 1 , Y \stackrel{\#}= ( k + j ) + 1 , z \in X , \forall f \, ( f \in S \Longleftrightarrow f \in X \to Y , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow S \stackrel{\#}= q \cdot ( ( k + j ) + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄 ，Ln ，∈∖1 ，LFibI ，Lex

1.4 個数の帰納法

\(0\) 個からの単射は空写像だけ（1 個）。
Lbase … \(j \in \mathbb{M} \Longrightarrow \forall U , V , G \, ( U \stackrel{\#}= 0 , V \stackrel{\#}= 0 + j , \forall f \, ( f \in G \Longleftrightarrow f \in U \to V , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow \exists q \in \mathbb{M} . G \stackrel{\#}= q , q \cdot j ! = ( 0 + j ) ! )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄
係数が一意であること、および \(q \cdot j! = (k+j)!\) から \((q \cdot ((k+j)+1)) \cdot j! = ((k+1)+j)!\)。
Lu1 … \(q , r , j \in \mathbb{M} , q \cdot j ! = r \cdot j ! \Longrightarrow q = r\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄 ，L!ℕ
Lar … \(q , k , j \in \mathbb{M} , q \cdot j ! = ( k + j ) ! \Longrightarrow ( q \cdot ( ( k + j ) + 1 ) ) \cdot j ! = ( ( k + 1 ) + j ) !\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄
帰納法の1歩：\(k\) について成り立てば \(k + 1\) について成り立つ（\(j\) は固定）。
Lstep … \(k , j \in \mathbb{M} , \forall U , V , G \, ( U \stackrel{\#}= k , V \stackrel{\#}= k + j , \forall f \, ( f \in G \Longleftrightarrow f \in U \to V , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow \exists q \in \mathbb{M} . G \stackrel{\#}= q , q \cdot j ! = ( k + j ) ! ) , U \stackrel{\#}= k + 1 , V \stackrel{\#}= ( k + 1 ) + j , \forall f \, ( f \in G \Longleftrightarrow f \in U \to V , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow \exists q \in \mathbb{M} . G \stackrel{\#}= q , q \cdot j ! = ( ( k + 1 ) + j ) !\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄 ，Ln ，∈∖1 ，LFibI ，Lex ，L!ℕ ，LIN ，Lu1 ，Lar
\(k\) についての帰納法（\(j\) は固定）。
Lind … \(k , j \in \mathbb{M} \Longrightarrow \forall U , V , G \, ( U \stackrel{\#}= k , V \stackrel{\#}= k + j , \forall f \, ( f \in G \Longleftrightarrow f \in U \to V , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow \exists q \in \mathbb{M} . G \stackrel{\#}= q , q \cdot j ! = ( k + j ) ! )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄 ，Ln ，∈∖1 ，LFibI ，Lex ，L!ℕ ，LIN ，Lbase ，Lu1 ，Lar ，Lstep

2 主定理

\(k\) 個の元の集合 \(X\) から \(k + j\) 個の元の集合 \(Y\) への単射の全体 \(G\) は \(q\) 個で、\(q \cdot j! = (k + j)!\)、つまり \(q = (k+j)!/j!\)。
\(k , j \in \mathbb{M} , X \stackrel{\#}= k , Y \stackrel{\#}= k + j , \forall f \, ( f \in G \Longleftrightarrow f \in X \to Y , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) \Longrightarrow \exists q \in \mathbb{M} . G \stackrel{\#}= q , q \cdot j ! = ( k + j ) !\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄 ，Ln ，∈∖1 ，LFibI ，Lex ，L!ℕ ，LIN ，Lbase ，Lu1 ，Lar ，Lstep ，Lind

2.1 全関数の個数

\(z \in X\) の像が \(a\) である写像の全体 \(F\) は、\(X \setminus \{z\}\) から \(Y\) への写像の全体 \(G\) と同じ個数（LFibI の単射でない版）。
LFibF … \(z \in X , a \in Y , \forall f \, ( f \in F \Longleftrightarrow f \in X \to Y , \langle z , a \rangle \in f ) , \forall g \, ( g \in G \Longleftrightarrow g \in X \mathop\setminus \{ z \} \to Y ) \Longrightarrow F \stackrel{\#}= G\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，Ln ，∈∖1
写像の全体は集合（\(X \to Y\)）。
LexF … \(\exists G \, \forall f \, ( f \in G \Longleftrightarrow f \in X \to Y )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(k\) 個から \(n\) 個への写像が \(q\) 個なら、\(k + 1\) 個から \(n\) 個への写像は \(q \cdot n\) 個。
LFN … \(k , n \in \mathbb{M} , q \in \mathbb{M} , \forall U , G \, ( U \stackrel{\#}= k , \forall f \, ( f \in G \Longleftrightarrow f \in U \to Y ) \Longrightarrow G \stackrel{\#}= q ) , X \stackrel{\#}= k + 1 , Y \stackrel{\#}= n , z \in X , \forall f \, ( f \in S \Longleftrightarrow f \in X \to Y ) \Longrightarrow S \stackrel{\#}= q \cdot n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，Ln ，∈∖1 ，LFibF ，LexF

2.2 全関数の個数の帰納法

\(0\) 個からの写像は空写像だけ（\(n^0 = 1\) 個）。
LbaseF … \(n \in \mathbb{M} \Longrightarrow \forall U , G \, ( U \stackrel{\#}= 0 , \forall f \, ( f \in G \Longleftrightarrow f \in U \to Y ) \Longrightarrow G \stackrel{\#}= n ^ 0 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄
LsF … \(k , n \in \mathbb{M} , Y \stackrel{\#}= n , \forall U , G \, ( U \stackrel{\#}= k , \forall f \, ( f \in G \Longleftrightarrow f \in U \to Y ) \Longrightarrow G \stackrel{\#}= n ^ { k } ) , U \stackrel{\#}= k + 1 , \forall f \, ( f \in G \Longleftrightarrow f \in U \to Y ) \Longrightarrow G \stackrel{\#}= n ^ { ( k + 1 ) }\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Ln ，∈∖1 ，LFibF ，LexF ，LFN
\(k\) についての帰納法（\(Y\) は \(n\) 個で固定）。
LindF … \(k , n \in \mathbb{M} , Y \stackrel{\#}= n \Longrightarrow \forall U , G \, ( U \stackrel{\#}= k , \forall f \, ( f \in G \Longleftrightarrow f \in U \to Y ) \Longrightarrow G \stackrel{\#}= n ^ k )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Ln ，∈∖1 ，LFibF ，LexF ，LFN ，LbaseF ，LsF
\(k\) 個の元の集合 \(X\) から \(n\) 個の元の集合 \(Y\) への写像の全体 \(G\) は \(n^k\) 個。
\(k , n \in \mathbb{M} , X \stackrel{\#}= k , Y \stackrel{\#}= n , \forall f \, ( f \in G \Longleftrightarrow f \in X \to Y ) \Longrightarrow G \stackrel{\#}= n ^ k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Ln ，∈∖1 ，LFibF ，LexF ，LFN ，LbaseF ，LsF ，LindF

3 誕生日の問題

\(k\) 人の誕生日が \(n = k + j\) 日のどれか。誕生日がすべて異なる場合は \(q\) 通りで \(q \cdot j! = n!\)、すべての場合は \(n^k\) 通り。誰も同じ日にならない確率は \(q / n^k\)。
\(k , j \in \mathbb{M} , X \stackrel{\#}= k , Y \stackrel{\#}= k + j , \forall f \, ( f \in G \Longleftrightarrow f \in X \to Y , \forall p , q , y \, ( \langle p , y \rangle \in f , \langle q , y \rangle \in f \Longrightarrow p = q ) ) , \forall f \, ( f \in H \Longleftrightarrow f \in X \to Y ) \Longrightarrow \exists q \in \mathbb{M} . G \stackrel{\#}= q , q \cdot j ! = ( k + j ) ! , H \stackrel{\#}= ( k + j ) ^ k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄 ，↑𝕄 ，Ln ，∈∖1 ，LFibI ，Lex ，L!ℕ ，LIN ，Lbase ，Lu1 ，Lar ，Lstep ，Lind ，LFibF ，LexF ，LFN ，LbaseF ，LsF ，LindF