---

Step * of Lemma fps-set-to-one-zero

∀[r:CRng]. ∀[y:Atom]. ∀[n:ℕ].  ([0]_n(y:=1) = 0 ∈ PowerSeries(r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Auto)
   THEN RepUR ``fps-zero fps-coeff fps-set-to-one`` 0
   THEN RepeatFor 2 ((AutoSplit THEN RW RngNormC 0 THEN Auto))
   THEN Auto') }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (BLemma  `fps-ext`  THEN  Auto)
  THEN  RepUR  ``fps-zero  fps-coeff  fps-set-to-one``  0
  THEN  RepeatFor  2  ((AutoSplit  THEN  RW  RngNormC  0  THEN  Auto))
  THEN  Auto')

---

Home Index