---

Step * of Lemma last_mklist

∀T:Type. ∀f:ℕ ⟶ T. ∀n:ℕ+.  (last(mklist(n;f)) = (f (n - 1)) ∈ T)
BY
{ Auto }

1
1. T : Type
2. f : ℕ ⟶ T
3. n : ℕ+
⊢ last(mklist(n;f)) = (f (n - 1)) ∈ T

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mforall{}n:\mBbbN{}\msupplus{}.    (last(mklist(n;f))  =  (f  (n  -  1)))


By

---

Latex:
Auto

---

Home Index