---

Step * of Lemma groupoid_inv

∀[G:Groupoid]
  ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) x y.
    (((cat-comp(cat(G)) x y x f groupoid-inv(G;x;y;f)) = (cat-id(cat(G)) x) ∈ (cat-arrow(cat(G)) x x))
    ∧ ((cat-comp(cat(G)) y x y groupoid-inv(G;x;y;f) f) = (cat-id(cat(G)) y) ∈ (cat-arrow(cat(G)) y y)))
BY
{ (Auto THEN D 1 THEN D 2 THEN All (RepUR ``groupoid-cat groupoid-inv``) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G:Groupoid]
    \mforall{}x,y:cat-ob(cat(G)).  \mforall{}f:cat-arrow(cat(G))  x  y.
        (((cat-comp(cat(G))  x  y  x  f  groupoid-inv(G;x;y;f))  =  (cat-id(cat(G))  x))
        \mwedge{}  ((cat-comp(cat(G))  y  x  y  groupoid-inv(G;x;y;f)  f)  =  (cat-id(cat(G))  y)))


By

---

Latex:
(Auto  THEN  D  1  THEN  D  2  THEN  All  (RepUR  ``groupoid-cat  groupoid-inv``)  THEN  Auto)

---

Home Index