---

Step * of Lemma nh-id-left

∀I,J:fset(ℕ). ∀f:I ⟶ J.  (f ⋅ 1 = f ∈ I ⟶ J)
BY
{ (Auto
   THEN RepUR ``nh-comp nh-id names-hom dma-lift-compose dM_inc`` 0
   THEN (FunExt THENA Auto)
   THEN Unfold `names-hom` -2
   THEN (InstLemma `free-dma-lift-id` [⌜names(I)⌝;⌜NamesDeq⌝]⋅ THENA Auto)
   THEN RepUR ``compose`` 0
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``nh-comp  nh-id  names-hom  dma-lift-compose  dM\_inc``  0
  THEN  (FunExt  THENA  Auto)
  THEN  Unfold  `names-hom`  -2
  THEN  (InstLemma  `free-dma-lift-id`  [\mkleeneopen{}names(I)\mkleeneclose{};\mkleeneopen{}NamesDeq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index