---

Step * of Lemma fps-summation-coeff

∀[X:Type]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].
  ∀m:bag(X). (fps-summation(r;b;x.f[x])[m] = Σ(x∈b). f[x][m] ∈ |r|)
BY
{ (Auto THEN BagToList (-2) THEN Auto) }

1
1. X : Type
2. r : CRng
3. T : Type
4. f : T ⟶ PowerSeries(X;r)
5. b : T List
6. m : bag(X)
⊢ fps-summation(r;b;x.f[x])[m] = Σ(x∈b). f[x][m] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  PowerSeries(X;r)].  \mforall{}[b:bag(T)].
    \mforall{}m:bag(X).  (fps-summation(r;b;x.f[x])[m]  =  \mSigma{}(x\mmember{}b).  f[x][m])


By

---

Latex:
(Auto  THEN  BagToList  (-2)  THEN  Auto)

---

Home Index