---

Step * 1 of Lemma fps-summation-coeff


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|
BY
{ (MoveToConcl (-2)
   THEN RepUR ``fps-summation bag-summation bag-accum fps-zero fps-add fps-coeff`` 0
   THEN InductionOnLast) }

1
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|

2
1. X : Type
2. r : CRng
3. T : Type
4. f : T ⟶ PowerSeries(X;r)
5. m : bag(X)
6. b : T List
7. ¬↑null(b)
8. ||b|| ≥ 1 
9. (accumulate (with value c and list item x):
     λb.(+r (f[x] b) (c b))
    over list:
      firstn(||b|| - 1;b)
    with starting value:
     λb.0) 
    m)
= accumulate (with value c and list item x):
   +r (f[x] m) c
  over list:
    firstn(||b|| - 1;b)
  with starting value:
   0)
∈ |r|
⊢ (accumulate (with value c and list item x):
    λb.(+r (f[x] b) (c b))
   over list:
     firstn(||b|| - 1;b) @ [last(b)]
   with starting value:
    λb.0) 
   m)
= accumulate (with value c and list item x):
   +r (f[x] m) c
  over list:
    firstn(||b|| - 1;b) @ [last(b)]
  with starting value:
   0)
∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  r  :  CRng
3.  T  :  Type
4.  f  :  T  {}\mrightarrow{}  PowerSeries(X;r)
5.  b  :  T  List
6.  m  :  bag(X)
\mvdash{}  fps-summation(r;b;x.f[x])[m]  =  \mSigma{}(x\mmember{}b).  f[x][m]


By

---

Latex:
(MoveToConcl  (-2)
  THEN  RepUR  ``fps-summation  bag-summation  bag-accum  fps-zero  fps-add  fps-coeff``  0
  THEN  InductionOnLast)

---

Home Index