---

Step * of Lemma fps-restrict-summation

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[d:bag(X)].
    (fps-restrict(eq;r;f;d) = Σ(x∈sub-bags(eq;d)). (f[x])*<x> ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN (Assert Assoc(PowerSeries(X;r);λf,g. (f+g)) ∧ Comm(PowerSeries(X;r);λf,g. (f+g)) BY
               (Auto THEN (D 0 THEN Reduce 0 THEN Auto) THEN FpsNorm 0 THEN Auto))
   THEN BLemma `fps-ext`
   THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. d : bag(X)
7. Assoc(PowerSeries(X;r);λf,g. (f+g))
8. Comm(PowerSeries(X;r);λf,g. (f+g))
9. b : bag(X)
⊢ fps-restrict(eq;r;f;d)[b] = Σ(x∈sub-bags(eq;d)). (f[x])*<x>[b] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f:PowerSeries(X;r)].  \mforall{}[d:bag(X)].
        (fps-restrict(eq;r;f;d)  =  \mSigma{}(x\mmember{}sub-bags(eq;d)).  (f[x])*<x>) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  (Assert  Assoc(PowerSeries(X;r);\mlambda{}f,g.  (f+g))  \mwedge{}  Comm(PowerSeries(X;r);\mlambda{}f,g.  (f+g))  BY
                          (Auto  THEN  (D  0  THEN  Reduce  0  THEN  Auto)  THEN  FpsNorm  0  THEN  Auto))
  THEN  BLemma  `fps-ext`
  THEN  Auto)

---

Home Index