---

Step * 2 of Lemma fps-deriv-commutes

.....subterm..... T:t
3:n
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)
⊢ (f x.y.b) = (f y.x.b) ∈ |r|
BY
{ EqCDA }

1
.....subterm..... T:t
2:n
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)

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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{}  (f  x.y.b)  =  (f  y.x.b)


By

---

Latex:
EqCDA

---

Home Index