---

Step * of Lemma rng_lsum-from-upto

∀[a,b:ℤ]. ∀[r:Rng]. ∀[f:{a..b-} ⟶ |r|].  (Σ{r} x ∈ [a, b). f[x] = (Σ(r) a ≤ i < b. f[i]) ∈ |r|)
BY
{ Assert ⌜∀n:ℕ
            ∀[a,b:ℤ].
              ∀[r:Rng]. ∀[f:{a..b-} ⟶ |r|].  (Σ{r} x ∈ [a, b). f[x] = (Σ(r) a ≤ i < b. f[i]) ∈ |r|) 
              supposing b ≤ (a + n)⌝⋅ }

1
.....assertion..... 
∀n:ℕ
  ∀[a,b:ℤ].
    ∀[r:Rng]. ∀[f:{a..b-} ⟶ |r|].  (Σ{r} x ∈ [a, b). f[x] = (Σ(r) a ≤ i < b. f[i]) ∈ |r|) supposing b ≤ (a + n)

2
1. ∀n:ℕ
     ∀[a,b:ℤ].
       ∀[r:Rng]. ∀[f:{a..b-} ⟶ |r|].  (Σ{r} x ∈ [a, b). f[x] = (Σ(r) a ≤ i < b. f[i]) ∈ |r|) supposing b ≤ (a + n)
⊢ ∀[a,b:ℤ]. ∀[r:Rng]. ∀[f:{a..b-} ⟶ |r|].  (Σ{r} x ∈ [a, b). f[x] = (Σ(r) a ≤ i < b. f[i]) ∈ |r|)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[r:Rng].  \mforall{}[f:\{a..b\msupminus{}\}  {}\mrightarrow{}  |r|].    (\mSigma{}\{r\}  x  \mmember{}  [a,  b).  f[x]  =  (\mSigma{}(r)  a  \mleq{}  i  <  b.  f[i]))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}
                    \mforall{}[a,b:\mBbbZ{}].
                        \mforall{}[r:Rng].  \mforall{}[f:\{a..b\msupminus{}\}  {}\mrightarrow{}  |r|].    (\mSigma{}\{r\}  x  \mmember{}  [a,  b).  f[x]  =  (\mSigma{}(r)  a  \mleq{}  i  <  b.  f[i])) 
                        supposing  b  \mleq{}  (a  +  n)\mkleeneclose{}\mcdot{}

---

Home Index