---

Step * of Lemma fps-deriv-commutes

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x,y:X].  (ddf/dx/dy = ddf/dy/dx ∈ PowerSeries(X;r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Auto)
   THEN RepUR ``fps-deriv fps-coeff`` 0
   THEN (RWO "rng_times_assoc" 0 THENA Auto)
   THEN 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)
⊢ (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|

2
.....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|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].  \mforall{}[x,y:X].
    (ddf/dx/dy  =  ddf/dy/dx)


By

---

Latex:
(Auto
  THEN  (BLemma  `fps-ext`  THEN  Auto)
  THEN  RepUR  ``fps-deriv  fps-coeff``  0
  THEN  (RWO  "rng\_times\_assoc"  0  THENA  Auto)
  THEN  EqCDA)

---

Home Index