---

Step * 2 1 1 of Lemma fps-deriv-commutes


1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. f : PowerSeries(X;r)
5. g : PowerSeries(X;r)
6. x : X
7. y : X
8. b : bag(X)
⊢ ({x} + {y} + b) = ({y} + {x} + b) ∈ bag(X)
BY
{ Auto }

---

Latex:

---

Latex:

1.  X  :  Type
2.  eq  :  EqDecider(X)
3.  r  :  CRng
4.  f  :  PowerSeries(X;r)
5.  g  :  PowerSeries(X;r)
6.  x  :  X
7.  y  :  X
8.  b  :  bag(X)
\mvdash{}  (\{x\}  +  \{y\}  +  b)  =  (\{y\}  +  \{x\}  +  b)


By

---

Latex:
Auto

---

Home Index