---

Step * of Lemma fps-exp_wf

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[n:ℕ].  ((f)^(n) ∈ PowerSeries(X;r)) supposing valueall-type(X)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f:PowerSeries(X;r)].  \mforall{}[n:\mBbbN{}].    ((f)\^{}(n)  \mmember{}  PowerSeries(X;r)) 
    supposing  valueall-type(X)


By

---

Latex:
ProveWfLemma

---

Home Index