---

Step * of Lemma bag-summation-reindex

∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
  ∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[h:A ⟶ T]. ∀[f:T ⟶ R].
    ∀[b:bag(T)]. (Σ(x∈b). f[x] = Σ(x∈bag-map(g;b)). f[h x] ∈ R) supposing ∀x:T. (x = (h (g x)) ∈ T) 
  supposing Comm(R;add) ∧ Assoc(R;add)
BY
{ ((UnivCD THENA Auto) THEN RWO "bag-summation-map" 0 THEN Auto THEN Auto THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].
    \mforall{}[T,A:Type].  \mforall{}[g:T  {}\mrightarrow{}  A].  \mforall{}[h:A  {}\mrightarrow{}  T].  \mforall{}[f:T  {}\mrightarrow{}  R].
        \mforall{}[b:bag(T)].  (\mSigma{}(x\mmember{}b).  f[x]  =  \mSigma{}(x\mmember{}bag-map(g;b)).  f[h  x])  supposing  \mforall{}x:T.  (x  =  (h  (g  x))) 
    supposing  Comm(R;add)  \mwedge{}  Assoc(R;add)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RWO  "bag-summation-map"  0
  THEN  Auto
  THEN  Auto
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index