---

Step * of Lemma name-morph-1-satisfies

∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I].  (1 f) = 1
BY
{ (Auto THEN RepUR ``name-morph-satisfies`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].    (1  f)  =  1


By

---

Latex:
(Auto  THEN  RepUR  ``name-morph-satisfies``  0  THEN  Auto)

---

Home Index