---

Step * 1 of Lemma dist_hom_over_mon_for


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|
BY
{ (ListInd 5 THEN AbReduce 0) }

1
1. T : Type
2. m : IMonoid
3. n : IMonoid
4. f : MonHom(m,n)
5. g : T ⟶ |m|
⊢ (f e) = e ∈ |n|

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

---

Latex:

---

Latex:

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


By

---

Latex:
(ListInd  5  THEN  AbReduce  0)

---

Home Index