---

Step * of Lemma bag-summation_wf

∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[f:T ⟶ R]. ∀[b:bag(T)].
  Σ(x∈b). f[x] ∈ R supposing Assoc(R;add) ∧ Comm(R;add)
BY
{ (ProveWfLemma⋅ THEN (Unfold `assoc` 7 THEN RWO "7" 0) THEN Auto THEN EqCD THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma\mcdot{}  THEN  (Unfold  `assoc`  7  THEN  RWO  "7"  0)  THEN  Auto  THEN  EqCD  THEN  Auto)

---

Home Index