---

Step * of Lemma cat-comp-ident

∀[C:SmallCategory]
  ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
    (((cat-comp(C) x x y (cat-id(C) x) f) = f ∈ (cat-arrow(C) x y))
    ∧ ((cat-comp(C) x y y f (cat-id(C) y)) = f ∈ (cat-arrow(C) x y)))
BY
{ ((UnivCD THENA Auto)
   THEN D 1
   THEN RepeatFor 3 (D -5)
   THEN All
   (RepUR ``cat-comp cat-arrow cat-ob cat-id``)⋅
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory]
    \mforall{}x,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.
        (((cat-comp(C)  x  x  y  (cat-id(C)  x)  f)  =  f)  \mwedge{}  ((cat-comp(C)  x  y  y  f  (cat-id(C)  y))  =  f))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  1
  THEN  RepeatFor  3  (D  -5)
  THEN  All
  (RepUR  ``cat-comp  cat-arrow  cat-ob  cat-id``)\mcdot{}
  THEN  All  Reduce
  THEN  Auto)

---

Home Index