---

Step * of Lemma psc-restriction-comp

No Annotations
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I).
  (g(f(a)) = cat-comp(C) K J I g f(a) ∈ X(K))
BY
{ (Auto
   THEN (Assert X ∈ ps_context{j:l}(C) BY
               Trivial)
   THEN DContext 2
   THEN RepUR ``psc-restriction`` 0
   THEN DCat 1
   THEN All (RepUR ``op-cat type-cat cat-ob cat-arrow cat-comp cat-id``)
   THEN RWO "10" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  X  \mmember{}  ps\_context\{j:l\}(C)  BY
                          Trivial)
  THEN  DContext  2
  THEN  RepUR  ``psc-restriction``  0
  THEN  DCat  1
  THEN  All  (RepUR  ``op-cat  type-cat  cat-ob  cat-arrow  cat-comp  cat-id``)
  THEN  RWO  "10"  0
  THEN  Auto)

---

Home Index