Calculation:
    (∑ i : ℕ ❙ i < k • m · i)[k ≔ 4]
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ (i < k)[k ≔ 4] • (m · i)[k ≔ 4]
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ i < 4 • m · i

Calculation:
    (∑ i : ℕ ❙ i < m • n · i)[m, n ≔ 3, 8]
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ (i < m)[m, n ≔ 3, 8] • (n · i)[m, n ≔ 3, 8]
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ (i < 3) • (8 · i)

Calculation:
    (∑ i : ℕ ❙ i < j • k · i)[i, j, k ≔ 2, 5, 8]
  =⟨ “Reflexivity of =” ⟩
    (∑ a : ℕ ❙ a < j • k · a)[i, j, k ≔ 2, 5, 8]
  =⟨ Substitution ⟩
    ∑ a : ℕ ❙ (a < j)[i, j, k ≔ 2, 5, 8] • (k · a)[i, j, k ≔ 2, 5, 8]
  =⟨ Substitution ⟩
    ∑ a : ℕ ❙ (a < 5) • (8 · a)


Calculation:
    (∑ i : ℕ ❙ i < k • m · i)[m ≔ i · j]
  =⟨ “Reflexivity of =” ⟩
    (∑ a : ℕ ❙ a < k • m · a)[m ≔ i · j]
  =⟨ Substitution ⟩
    ∑ a : ℕ ❙ (a < k)[m ≔ i · j] • (m · a)[m ≔ i · j]
  =⟨ Substitution ⟩
    ∑ a : ℕ ❙ (a < k) • (i · j · a)

Calculation:
    (∑ i : ℕ ❙ i < k • (∑ j : ℕ ❙ j < i • m · j))[m ≔ j + k]
  =⟨ “Reflexivity of =” ⟩
    (∑ i : ℕ ❙ i < k • (∑ a : ℕ ❙ a < i • m · a))[m ≔ j + k]
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ (i < k)[m ≔ j + k] • (∑ a : ℕ ❙ a < i • m · a)[m ≔ j + k]
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ (i < k)[m ≔ j + k] • (∑ a : ℕ ❙ (a < i)[m ≔ j + k] • (m · a)[m ≔ j + k])
  =⟨ Substitution ⟩
    ∑ i : ℕ ❙ (i < k) • (∑ a : ℕ ❙ (a < i) • ((j + k) · a))


Calculation:
    (∑ i : ℕ ❙ i < k • (∑ j : ℕ ❙ j < i • m · j))[k ≔ 2 · i]
  =⟨ “Reflexivity of =” ⟩
    (∑ a : ℕ ❙ a < k • (∑ j : ℕ ❙ j < a • m · j))[k ≔ 2 · i]
  =⟨ Substitution ⟩
    (∑ a : ℕ ❙ (a < k)[k ≔ 2 · i] • (∑ j : ℕ ❙ j < a • m · j)[k ≔ 2 · i])
  =⟨ Substitution ⟩
    (∑ a : ℕ ❙ (a < k)[k ≔ 2 · i] • (∑ j : ℕ ❙ (j < a)[k ≔ 2 · i] • (m · j)[k ≔ 2 · i]))
  =⟨ Substitution ⟩
    (∑ a : ℕ ❙ (a < 2 · i) • (∑ j : ℕ ❙ (j < a) • (m · j)))


Calculation:
    (∑ i : ℕ ❙ i < k • (∑ j : ℕ ❙ j < i • m · j))[m ≔ i · j]
  =⟨ “Reflexivity of =” ⟩
    (∑ a : ℕ ❙ a < k • (∑ j : ℕ ❙ j < a • m · j))[m ≔ i · j]
  =⟨ “Reflexivity of =” ⟩
    (∑ a : ℕ ❙ a < k • (∑ b : ℕ ❙ b < a • m · b))[m ≔ i · j]
  =⟨ Substitution ⟩
    (∑ a : ℕ ❙ (a < k)[m ≔ i · j] • (∑ b : ℕ ❙ b < a • m · b)[m ≔ i · j])
  =⟨ Substitution ⟩
    (∑ a : ℕ ❙ (a < k)[m ≔ i · j] • (∑ b : ℕ ❙ (b < a)[m ≔ i · j] • (m · b)[m ≔ i · j]))
  =⟨ Substitution ⟩
    (∑ a : ℕ ❙ (a < k) • (∑ b : ℕ ❙ (b < a) • (i · j · b)))