---

Step * of Lemma dM-lift-unique-fun

∀[I,J:fset(ℕ)]. ∀[f:I ⟶ J]. ∀[g:dma-hom(dM(J);dM(I))].
  dM-lift(I;J;f) = g ∈ (Point(dM(J)) ⟶ Point(dM(I))) supposing ∀j:names(J). ((g <j>) = (f j) ∈ Point(dM(I)))
BY
{ (InstLemma `dM-lift-unique` [] THEN RepeatFor 6 (ParallelLast')) }

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:I  {}\mrightarrow{}  J].  \mforall{}[g:dma-hom(dM(J);dM(I))].
    dM-lift(I;J;f)  =  g  supposing  \mforall{}j:names(J).  ((g  <j>)  =  (f  j))


By

---

Latex:
(InstLemma  `dM-lift-unique`  []  THEN  RepeatFor  6  (ParallelLast'))

---

Home Index