---

Step * of Lemma dist_hom_over_mon_for

∀T:Type. ∀m,n:IMonoid. ∀f:MonHom(m,n). ∀a:T List. ∀g:T ⟶ |m|.
  ((f (For{m} x ∈ a. g[x])) = (For{n} x ∈ a. (f g[x])) ∈ |n|)
BY
{ Auto }

1
1. T : Type
2. m : IMonoid
3. n : IMonoid
4. f : MonHom(m,n)
5. a : T List
6. g : T ⟶ |m|
⊢ (f (For{m} x ∈ a. g[x])) = (For{n} x ∈ a. (f g[x])) ∈ |n|

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}m,n:IMonoid.  \mforall{}f:MonHom(m,n).  \mforall{}a:T  List.  \mforall{}g:T  {}\mrightarrow{}  |m|.
    ((f  (For\{m\}  x  \mmember{}  a.  g[x]))  =  (For\{n\}  x  \mmember{}  a.  (f  g[x])))


By

---

Latex:
Auto

---

Home Index