---

Step * of Lemma double_sum_functionality

∀[n,m:ℕ]. ∀[f,g:ℕn ⟶ ℕm ⟶ ℤ].
  sum(f[x;y] | x < n; y < m) = sum(g[x;y] | x < n; y < m) ∈ ℤ supposing ∀x:ℕn. ∀y:ℕm.  (f[x;y] = g[x;y] ∈ ℤ)
BY
{ (Auto
   THEN Unfold `double_sum` 0
   THEN BackThruLemma `sum_functionality`
   THEN Try (Complete (Auto))
   THEN D 0
   THEN EasyHyp
   THEN Auto
   THEN BackThruLemma `sum_functionality`
   THEN Try (Complete (Auto))
   THEN D 0
   THEN EasyHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m  {}\mrightarrow{}  \mBbbZ{}].
    sum(f[x;y]  |  x  <  n;  y  <  m)  =  sum(g[x;y]  |  x  <  n;  y  <  m)  supposing  \mforall{}x:\mBbbN{}n.  \mforall{}y:\mBbbN{}m.    (f[x;y]  =  g[x;y])


By

---

Latex:
(Auto
  THEN  Unfold  `double\_sum`  0
  THEN  BackThruLemma  `sum\_functionality`
  THEN  Try  (Complete  (Auto))
  THEN  D  0
  THEN  EasyHyp
  THEN  Auto
  THEN  BackThruLemma  `sum\_functionality`
  THEN  Try  (Complete  (Auto))
  THEN  D  0
  THEN  EasyHyp
  THEN  Auto)

---

Home Index