---

Step * 1 of Lemma fps-add-assoc


1. X : Type
2. r : CRng
3. f : PowerSeries(X;r)
4. g : PowerSeries(X;r)
5. h : PowerSeries(X;r)
6. IsRing(|r|;+r;0;-r;*;1)
⊢ ((f+g)+h) = (f+(g+h)) ∈ PowerSeries(X;r)
BY
{ (BLemma `fps-ext` THEN Auto THEN RepUR ``fps-add fps-coeff`` 0 THEN Fold `infix_ap` 0 THEN Fold `fps-coeff` 0)⋅ }

1
1. X : Type
2. r : CRng
3. f : PowerSeries(X;r)
4. g : PowerSeries(X;r)
5. h : PowerSeries(X;r)
6. IsRing(|r|;+r;0;-r;*;1)
7. b : bag(X)
⊢ ((f[b] +r g[b]) +r h[b]) = (f[b] +r (g[b] +r h[b])) ∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  r  :  CRng
3.  f  :  PowerSeries(X;r)
4.  g  :  PowerSeries(X;r)
5.  h  :  PowerSeries(X;r)
6.  IsRing(|r|;+r;0;-r;*;1)
\mvdash{}  ((f+g)+h)  =  (f+(g+h))


By

---

Latex:
(BLemma  `fps-ext`
  THEN  Auto
  THEN  RepUR  ``fps-add  fps-coeff``  0
  THEN  Fold  `infix\_ap`  0
  THEN  Fold  `fps-coeff`  0)\mcdot{}

---

Home Index