---

Step * 1 of Lemma fps-mul-comm


1. X : Type
2. eq : EqDecider(X)
3. valueall-type(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. b : bag(X)
8. Assoc(|r|;+r)
9. Comm(|r|;+r)
⊢ Σ(p∈bag-partitions(eq;b)). f[fst(p)] * g[snd(p)]
= Σ(p∈bag-map(λp.<snd(p), fst(p)>;bag-partitions(eq;b))). g[fst(p)] * f[snd(p)]
∈ |r|
BY
{ xxx((RWO "bag-summation-map" 0 THENA Auto) THEN Reduce 0 THEN EqCD THEN Auto)xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  eq  :  EqDecider(X)
3.  valueall-type(X)
4.  r  :  CRng
5.  f  :  PowerSeries(X;r)
6.  g  :  PowerSeries(X;r)
7.  b  :  bag(X)
8.  Assoc(|r|;+r)
9.  Comm(|r|;+r)
\mvdash{}  \mSigma{}(p\mmember{}bag-partitions(eq;b)).  f[fst(p)]  *  g[snd(p)]
=  \mSigma{}(p\mmember{}bag-map(\mlambda{}p.<snd(p),  fst(p)>bag-partitions(eq;b))).  g[fst(p)]  *  f[snd(p)]


By

---

Latex:
xxx((RWO  "bag-summation-map"  0  THENA  Auto)  THEN  Reduce  0  THEN  EqCD  THEN  Auto)xxx

---

Home Index