---

Step * of Lemma poset-functor-id

∀[I:Cname List]. ∀[f:name-morph(I;I)].
  poset-functor(I;I;f) = 1 ∈ Functor(poset-cat(I);poset-cat(I)) supposing f = 1 ∈ name-morph(I;I)
BY
{ (Auto THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[f:name-morph(I;I)].    poset-functor(I;I;f)  =  1  supposing  f  =  1


By

---

Latex:
(Auto  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index