---

Step * of Lemma cube-set-restriction-comp2

No Annotations
∀X:j⊢. ∀I,J1,J2,K:fset(ℕ). ∀f:J1 ⟶ I. ∀g:K ⟶ J1. ∀a:X(I).  g(f(a)) = f ⋅ g(a) ∈ X(K) supposing J1 = J2 ∈ fset(ℕ)
BY
{ PresheafMLTTInstance Obid: psc-restriction-comp2⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}I,J1,J2,K:fset(\mBbbN{}).  \mforall{}f:J1  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J1.  \mforall{}a:X(I).    g(f(a))  =  f  \mcdot{}  g(a)  supposing  J1  =  J2


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-restriction-comp2\mcdot{}

---

Home Index