べき乗の和：\(\sum_{i=0}^{n} i^2 = \frac{n(n+1)(2n+1)}{6}\)（2乗）と \(\sum_{i=0}^{n} i^3 = \left(\frac{n(n+1)}{2}\right)^2\)（3乗）。自然数には割り算が無いので、両辺を 6 倍・4 倍した形で述べる。
和は articles2/Seq の \(f\ \mathrm{sum}\ n\)（第 0 項から第 \(n-1\) 項まで）。\(i = 0, \ldots, n\) の和は \(f\ \mathrm{sum}\ (n+1)\)。

1 準備

3乗の和の帰納法の1歩：\(4u = m^2(m+1)^2\) ならば \(4(u + (m+1)^3) = (m+1)^2(m+2)^2\)。
2乗を ↑ で書いた形（Lar⋅2 の言い換え）。
3乗を ↑ で書いた形（Lar⋅3 の言い換え）。

2 主定理（k = 2）

第 \(i\) 項が \(i^2\) の列 \(f\) について、\(i = 0, \ldots, n\) の和 \(f\ \mathrm{sum}\ (n+1)\) は 6 倍すると右辺になる。
\(\forall i \in \mathbb{M} . f ( i ) = i ^ 2 , n \in \mathbb{M} \Longrightarrow 6 \cdot ( f \sum ( n + 1 ) ) = n \cdot ( ( n + 1 ) \cdot ( 2 \cdot n + 1 ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，sum𝕄

3 主定理（k = 3）

第 \(i\) 項が \(i^3\) の列 \(f\) について、\(i = 0, \ldots, n\) の和 \(f\ \mathrm{sum}\ (n+1)\) は 4 倍すると右辺になる。
\(\forall i \in \mathbb{M} . f ( i ) = i ^ 3 , n \in \mathbb{M} \Longrightarrow 4 \cdot ( f \sum ( n + 1 ) ) = n ^ 2 \cdot ( n + 1 ) ^ 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，sum𝕄