---

Step * of Lemma dist_hom_over_mset_for

∀s:DSet. ∀m,n:IAbMonoid. ∀f:MonHom(m,n). ∀a:MSet{s}. ∀g:|s| ⟶ |m|.
  ((f (msFor{m} x ∈ a. g[x])) = (msFor{n} x ∈ a. (f g[x])) ∈ |n|)
BY
{ ((RepeatMFor 4 (D 0)) THENA Auto) }

1
1. s : DSet@i'
2. m : IAbMonoid@i'
3. n : IAbMonoid@i'
4. f : MonHom(m,n)@i
⊢ ∀a:MSet{s}. ∀g:|s| ⟶ |m|.  ((f (msFor{m} x ∈ a. g[x])) = (msFor{n} x ∈ a. (f g[x])) ∈ |n|)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}m,n:IAbMonoid.  \mforall{}f:MonHom(m,n).  \mforall{}a:MSet\{s\}.  \mforall{}g:|s|  {}\mrightarrow{}  |m|.
    ((f  (msFor\{m\}  x  \mmember{}  a.  g[x]))  =  (msFor\{n\}  x  \mmember{}  a.  (f  g[x])))


By

---

Latex:
((RepeatMFor  4  (D  0))  THENA  Auto)

---

Home Index