2 主定理

\(s(n)(m)\) を \(\sum_{k\lt m} \binom{n}{k} a^k b^{n-k}\) とします。自然数には引き算が無いので、\(k + j = n\) と書いて \(b^{n-k}\) を \(b^j\) で表し、\(s\) を \(s(n)(0) = 0\) と漸化式 \(s(k+j)(k+1) = s(k+j)(k) + \binom{k+j}{k} a^k b^j\) を満たす関数として仮定します（補題 Bin。そのような \(s\) が在ることは、最後の定理でパラメータ付きの再帰定理 REC2 から示します）。
証明の要は \(s(n+1)(m+1) = b\,s(n)(m+1) + a\,s(n)(m)\)（\(m \le n\)・パスカルの漸化式から \(m\) についての帰納法）です。
Bin … \(a , b \in \mathbb{M} , \forall n \in \mathbb{M} . ( ( s ( n ) ) ( 0 ) ) = 0 , \forall k \in \mathbb{M} . \forall j \in \mathbb{M} . ( ( s ( ( k + j ) ) ) ( ( k + 1 ) ) ) = ( ( s ( ( k + j ) ) ) ( k ) ) + ( ( k + j ) \mathrm{C} k ) \cdot ( a ^ k \cdot b ^ j ) , n \in \mathbb{M} \Longrightarrow ( a + b ) ^ n = ( ( s ( n ) ) ( ( n + 1 ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅ℕ ，⋅𝕄0 ，↑ℕ ，↑𝕄0 ，ℙ.' ，\(0 \in \mathbb{M}\) ，choose𝕄 ，choose∈𝕄 ，Lnn ，Labs