---

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

∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[y:Atom]. ∀[n:ℕ].  ([(f-g)]_n(y:=1) = ([f]_n(y:=1)-[g]_n(y:=1)) ∈ PowerSeries(r))
BY
{ (xxxUnfold `fps-sub` 0xxx THEN Auto THEN RWW "fps-set-to-one-add fps-set-to-one-neg" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(xxxUnfold  `fps-sub`  0xxx  THEN  Auto  THEN  RWW  "fps-set-to-one-add  fps-set-to-one-neg"  0  THEN  Auto)

---

Home Index