---

Step * 1 1 1 of Lemma compose_wf_for_mon_hom


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)
BY
{ ((OnCls [0;5;7] (RepUnfolds ``monoid_hom_p fun_thru_2op``)) THEN Auto) }

1
1. A : IMonoid
2. B : IMonoid
3. C : IMonoid
4. f : |A| ⟶ |B|
5. ∀[a1,a2:|A|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |B|)
6. (f e) = e ∈ |B|
7. g : |B| ⟶ |C|
8. ∀[a1,a2:|B|].  ((g (a1 * a2)) = ((g a1) * (g a2)) ∈ |C|)
9. (g e) = e ∈ |C|
10. a1 : |A|
11. a2 : |A|
⊢ ((g o f) (a1 * a2)) = (((g o f) a1) * ((g o f) a2)) ∈ |C|

---

Latex:

---

Latex:

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


By

---

Latex:
((OnCls  [0;5;7]  (RepUnfolds  ``monoid\_hom\_p  fun\_thru\_2op``))  THEN  Auto)

---

Home Index