---

Step * of Lemma converges-to_functionality2

∀x1,x2:ℕ ⟶ ℝ. ∀y1,y2:ℝ.  (lim n→∞.x1[n] = y1 ⇒ lim n→∞.x2[n] = y2) supposing ((y1 = y2) and (∀n:ℕ. (x1[n] = x2[n])))
BY
{ (InstLemma `converges-to_functionality` [] THEN Unfold `guard` -1 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}x1,x2:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}y1,y2:\mBbbR{}.
    (lim  n\mrightarrow{}\minfty{}.x1[n]  =  y1  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x2[n]  =  y2)  supposing  ((y1  =  y2)  and  (\mforall{}n:\mBbbN{}.  (x1[n]  =  x2[n])))


By

---

Latex:
(InstLemma  `converges-to\_functionality`  []  THEN  Unfold  `guard`  -1  THEN  Trivial)

---

Home Index