---

Step * 2 of Lemma fps-compose-one


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. f : PowerSeries(X;r)
7. bs : bag(X)
8. ¬(bs = {} ∈ bag(X))
⊢ Σ(L∈bag-parts'(eq;bs;x)). if bag-null(hd(L) + bag-rep(||tl(L)||;x)) then 1 else 0 fi  * Πa ∈ tl(L). f a = 0 ∈ |r|
BY
{ xxx((Assert Comm(|r|;*) ∧ Assoc(|r|;*) ∧ IsMonoid(|r|;+r;0) ∧ Comm(|r|;+r) BY
             (RepeatFor 2 ((DVar `r'⋅ THEN Auto))
              THEN (InstLemma `rng_plus_comm` [⌜r⌝]⋅ THEN Auto)
              THEN Fold `comm` (-1)
              THEN Auto))
      THEN Using [`T',⌜bag(X) List+⌝] (BLemma `bag-summation-is-zero`)⋅
      THEN Auto
      THEN Auto)xxx }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. f : PowerSeries(X;r)
7. bs : bag(X)
8. ¬(bs = {} ∈ bag(X))
9. Comm(|r|;*)
10. Assoc(|r|;*)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. L : bag(X) List+
14. L ↓∈ bag-parts'(eq;bs;x)
⊢ (if bag-null(hd(L) + bag-rep(||tl(L)||;x)) then 1 else 0 fi  * Πa ∈ tl(L). f a) = 0 ∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  x  :  X
6.  f  :  PowerSeries(X;r)
7.  bs  :  bag(X)
8.  \mneg{}(bs  =  \{\})
\mvdash{}  \mSigma{}(L\mmember{}bag-parts'(eq;bs;x)).  if  bag-null(hd(L)  +  bag-rep(||tl(L)||;x))  then  1  else  0  fi   
                                                        * 
                                                        \mPi{}a  \mmember{}  tl(L).  f  a
=  0


By

---

Latex:
xxx((Assert  Comm(|r|;*)  \mwedge{}  Assoc(|r|;*)  \mwedge{}  IsMonoid(|r|;+r;0)  \mwedge{}  Comm(|r|;+r)  BY
                      (RepeatFor  2  ((DVar  `r'\mcdot{}  THEN  Auto))
                        THEN  (InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THEN  Auto)
                        THEN  Fold  `comm`  (-1)
                        THEN  Auto))
        THEN  Using  [`T',\mkleeneopen{}bag(X)  List\msupplus{}\mkleeneclose{}]  (BLemma  `bag-summation-is-zero`)\mcdot{}
        THEN  Auto
        THEN  Auto)xxx

---

Home Index