---

Step * of Lemma fps-set-to-one_wf

∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([f]_n(y:=1) ∈ PowerSeries(r))
BY
{ (ProveWfLemma THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[f:PowerSeries(r)].  \mforall{}[y:Atom].  \mforall{}[n:\mBbbN{}].    ([f]\_n(y:=1)  \mmember{}  PowerSeries(r))


By

---

Latex:
(ProveWfLemma  THEN  Auto')

---

Home Index