---

Step * of Lemma fps-scalar-mul-rng-add

∀[X:Type]. ∀[r:CRng]. ∀[c1,c2:|r|]. ∀[f:PowerSeries(X;r)].  ((c1 +r c2)*f = ((c1)*f+(c2)*f) ∈ PowerSeries(X;r))
BY
{ xxx((xxxAutoxxx THEN BLemma `fps-ext`  THEN Auto) THEN FpsCompute 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[c1,c2:|r|].  \mforall{}[f:PowerSeries(X;r)].    ((c1  +r  c2)*f  =  ((c1)*f+(c2)*f))


By

---

Latex:
xxx((xxxAutoxxx  THEN  BLemma  `fps-ext`    THEN  Auto)  THEN  FpsCompute  0  THEN  Auto)xxx

---

Home Index