---

Step * of Lemma fps-elim-x-add

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[f,g:PowerSeries(X;r)].  ((f+g)(x:=0) = (f(x:=0)+g(x:=0)) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ ((InstLemma `fps-elim-hom` [] THEN ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (D -2 THENA Auto)
   THEN RepeatFor 3 (ParallelLast')
   THEN Unfold `fun_thru_2op` -1
   THEN Reduce (-1)
   THEN Unfold `fps-elim-x` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].  \mforall{}[f,g:PowerSeries(X;r)].
        ((f+g)(x:=0)  =  (f(x:=0)+g(x:=0))) 
    supposing  valueall-type(X)


By

---

Latex:
((InstLemma  `fps-elim-hom`  []  THEN  ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Unfold  `fun\_thru\_2op`  -1
  THEN  Reduce  (-1)
  THEN  Unfold  `fps-elim-x`  0
  THEN  Auto)

---

Home Index