---

Step * 1 1 of Lemma fps-summation-coeff


1. X : Type
2. r : CRng
3. T : Type
4. f : T ⟶ PowerSeries(X;r)
5. m : bag(X)
⊢ (accumulate (with value c and list item x): λb.(+r (f[x] b) (c b))over list:  []with starting value: λb.0) m)
= accumulate (with value c and list item x):
   +r (f[x] m) c
  over list:
    []
  with starting value:
   0)
∈ |r|
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  r  :  CRng
3.  T  :  Type
4.  f  :  T  {}\mrightarrow{}  PowerSeries(X;r)
5.  m  :  bag(X)
\mvdash{}  (accumulate  (with  value  c  and  list  item  x):
        \mlambda{}b.(+r  (f[x]  b)  (c  b))
      over  list:
          []
      with  starting  value:
        \mlambda{}b.0) 
      m)
=  accumulate  (with  value  c  and  list  item  x):
      +r  (f[x]  m)  c
    over  list:
        []
    with  starting  value:
      0)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index