---

Step * of Lemma left-right-inverse-unique

∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g2:cat-arrow(C) y x].
  ∀[g1:cat-arrow(C) y x]. g1 = g2 ∈ (cat-arrow(C) y x) supposing fg1=1 supposing g2f=1
BY
{ Auto }

1
1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. f : cat-arrow(C) x y
5. g2 : cat-arrow(C) y x
6. g2f=1
7. g1 : cat-arrow(C) y x
8. fg1=1
⊢ g1 = g2 ∈ (cat-arrow(C) y x)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[x,y:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  x  y].  \mforall{}[g2:cat-arrow(C)  y  x].
    \mforall{}[g1:cat-arrow(C)  y  x].  g1  =  g2  supposing  fg1=1  supposing  g2f=1


By

---

Latex:
Auto

---

Home Index