---

Step * of Lemma group-cat_wf

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

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

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

---

Latex:

---

Latex:
No  Annotations
Group  \mmember{}  SmallCategory'


By

---

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

---

Home Index