---

Step * of Lemma group-cat_wf

Group ∈ SmallCategory'
BY
{ (ProveWfLemma THEN Try (((DVar `f' THENA Auto) THEN Symmetry THEN EqTypeCD THEN Auto))) }

1
1. G : Group{i}
⊢ λx.x ∈ MonHom(G,G)

2
.....set predicate..... 
1. G : Group{i}
2. H : Group{i}
3. z : Group{i}
4. K : Group{i}
5. f : |G| ⟶ |H|
6. IsMonHom{G,H}(f)
7. g : MonHom(H,z)
8. h : MonHom(z,K)
⊢ IsMonHom{G,K}((h o g) o f)

---

Latex:

---

Latex:
Group  \mmember{}  SmallCategory'


By

---

Latex:
(ProveWfLemma  THEN  Try  (((DVar  `f'  THENA  Auto)  THEN  Symmetry  THEN  EqTypeCD  THEN  Auto)))

---

Home Index