---

Step * 1 of Lemma compose_wf_for_mon_hom


1. A : IMonoid
2. B : IMonoid
3. C : IMonoid
4. f : MonHom(A,B)
5. g : MonHom(B,C)
⊢ g o f ∈ MonHom(A,C)
BY
{ ((MemTypeCD) THEN Auto) }

1
.....set predicate..... 
1. A : IMonoid
2. B : IMonoid
3. C : IMonoid
4. f : MonHom(A,B)
5. g : MonHom(B,C)
⊢ IsMonHom{A,C}(g o f)

---

Latex:

---

Latex:

1.  A  :  IMonoid
2.  B  :  IMonoid
3.  C  :  IMonoid
4.  f  :  MonHom(A,B)
5.  g  :  MonHom(B,C)
\mvdash{}  g  o  f  \mmember{}  MonHom(A,C)


By

---

Latex:
((MemTypeCD)  THEN  Auto)

---

Home Index