---

Step * 1 of Lemma fps-deriv-commutes

.....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)
⊢ (int-to-ring(r;(#y in b) + 1) * int-to-ring(r;(#x in y.b) + 1))
= (int-to-ring(r;(#x in b) + 1) * int-to-ring(r;(#y in x.b) + 1))
∈ |r|
BY
{ (RWO "bag-count-cons" 0 THEN Auto) }

---

Latex:

---

Latex:
.....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)
\mvdash{}  (int-to-ring(r;(\#y  in  b)  +  1)  *  int-to-ring(r;(\#x  in  y.b)  +  1))
=  (int-to-ring(r;(\#x  in  b)  +  1)  *  int-to-ring(r;(\#y  in  x.b)  +  1))


By

---

Latex:
(RWO  "bag-count-cons"  0  THEN  Auto)

---

Home Index