---

Step * of Lemma nc-e-same

No Annotations
∀I:fset(ℕ). ∀z:ℕ.  (e(z;z) = 1 ∈ I+z ⟶ I+z)
BY
{ (Auto THEN Unfold `names-hom` 0 THEN FunExt THEN Auto THEN RepUR ``nc-e nh-id`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:fset(\mBbbN{}).  \mforall{}z:\mBbbN{}.    (e(z;z)  =  1)


By

---

Latex:
(Auto  THEN  Unfold  `names-hom`  0  THEN  FunExt  THEN  Auto  THEN  RepUR  ``nc-e  nh-id``  0  THEN  AutoSplit)

---

Home Index