---

Step * 1 1 of Lemma compose_wf_for_mon_hom

.....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)
BY
{ ((D 5 THENM D 4) THENA Auto) }

1
1. A : IMonoid
2. B : IMonoid
3. C : IMonoid
4. f : |A| ⟶ |B|
5. IsMonHom{A,B}(f)
6. g : |B| ⟶ |C|
7. IsMonHom{B,C}(g)
⊢ IsMonHom{A,C}(g o f)

---

Latex:

---

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


By

---

Latex:
((D  5  THENM  D  4)  THENA  Auto)

---

Home Index