---

Step * of Lemma fps-mul-slice

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n:ℕ]. ∀[f,g:PowerSeries(X;r)].
    ([(f*g)]_n = fps-summation(r;upto(n + 1);k.([f]_k*[g]_n - k)) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN (Assert Assoc(|r|;+r) ∧ Comm(|r|;+r) BY
               (Auto
                THEN (InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
                THEN Fold `comm` (-1)
                THEN Auto
                THEN RepeatFor 2 ((DVar `r' THEN Auto))))
   THEN Unfold `power-series` 0
   THEN Ext
   THEN Auto
   THEN Try ((Fold `power-series` 0 THEN Auto))
   THEN Assert ⌜upto(n + 1) ∈ bag(ℕ)⌝⋅
   THEN Auto
   THEN Fold `fps-coeff` 0
   THEN RWO "fps-summation-coeff" 0
   THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℕ
6. f : PowerSeries(X;r)
7. g : PowerSeries(X;r)
8. Assoc(|r|;+r)
9. Comm(|r|;+r)
10. x : bag(X)
11. upto(n + 1) ∈ bag(ℕ)
⊢ [(f*g)]_n[x] = Σ(k∈upto(n + 1)). ([f]_k*[g]_n - k)[x] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[f,g:PowerSeries(X;r)].
        ([(f*g)]\_n  =  fps-summation(r;upto(n  +  1);k.([f]\_k*[g]\_n  -  k))) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  (Assert  Assoc(|r|;+r)  \mwedge{}  Comm(|r|;+r)  BY
                          (Auto
                            THEN  (InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  Fold  `comm`  (-1)
                            THEN  Auto
                            THEN  RepeatFor  2  ((DVar  `r'  THEN  Auto))))
  THEN  Unfold  `power-series`  0
  THEN  Ext
  THEN  Auto
  THEN  Try  ((Fold  `power-series`  0  THEN  Auto))
  THEN  Assert  \mkleeneopen{}upto(n  +  1)  \mmember{}  bag(\mBbbN{})\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Fold  `fps-coeff`  0
  THEN  RWO  "fps-summation-coeff"  0
  THEN  Auto)

---

Home Index