---

Step * 2 of Lemma mon_hom_p_comp


1. g : GrpSig
2. h : GrpSig
3. k : GrpSig
4. r : |g| ⟶ |h|
5. s : |h| ⟶ |k|
6. ∀[a1,a2:|g|].  ((r (a1 * a2)) = ((r a1) * (r a2)) ∈ |h|)
7. (r e) = e ∈ |h|
8. ∀[a1,a2:|h|].  ((s (a1 * a2)) = ((s a1) * (s a2)) ∈ |k|)
9. (s e) = e ∈ |k|
⊢ (s (r e)) = e ∈ |k|
BY
{ ((RWW "7 9" 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  h  :  GrpSig
3.  k  :  GrpSig
4.  r  :  |g|  {}\mrightarrow{}  |h|
5.  s  :  |h|  {}\mrightarrow{}  |k|
6.  \mforall{}[a1,a2:|g|].    ((r  (a1  *  a2))  =  ((r  a1)  *  (r  a2)))
7.  (r  e)  =  e
8.  \mforall{}[a1,a2:|h|].    ((s  (a1  *  a2))  =  ((s  a1)  *  (s  a2)))
9.  (s  e)  =  e
\mvdash{}  (s  (r  e))  =  e


By

---

Latex:
((RWW  "7  9"  0)  THEN  Auto)

---

Home Index