---

Step * of Lemma fps-set-to-one-scalar-mul

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


By

---

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

---

Home Index