---

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

∀[r:CRng]. ∀[f:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([-(f)]_n(y:=1) = -([f]_n(y:=1)) ∈ PowerSeries(r))
BY
{ (Auto
   THEN (BLemma `fps-ext` THEN Auto)
   THEN RepUR ``fps-neg 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{}[f:PowerSeries(r)].  \mforall{}[y:Atom].  \mforall{}[n:\mBbbN{}].    ([-(f)]\_n(y:=1)  =  -([f]\_n(y:=1)))


By

---

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

---

Home Index