---

Step * 1 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|
10. a1 : |g|
11. a2 : |g|
⊢ (s (r (a1 * a2))) = ((s (r a1)) * (s (r a2))) ∈ |k|
BY
{ ((RWW "6 8" 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
10.  a1  :  |g|
11.  a2  :  |g|
\mvdash{}  (s  (r  (a1  *  a2)))  =  ((s  (r  a1))  *  (s  (r  a2)))


By

---

Latex:
((RWW  "6  8"  0)  THEN  Auto)

---

Home Index