---

Step * of Lemma psc-restriction-comp2

No Annotations
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀I,J1,J2,K:cat-ob(C). ∀f:cat-arrow(C) J1 I. ∀g:cat-arrow(C) K J1. ∀a:X(I).
  g(f(a)) = cat-comp(C) K J1 I g f(a) ∈ X(K) supposing J1 = J2 ∈ cat-ob(C)
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X:ps\_context\{j:l\}(C).  \mforall{}I,J1,J2,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J1  I.
\mforall{}g:cat-arrow(C)  K  J1.  \mforall{}a:X(I).
    g(f(a))  =  cat-comp(C)  K  J1  I  g  f(a)  supposing  J1  =  J2


By

---

Latex:
Auto

---

Home Index