---

Step * of Lemma fps-mul-coeff0

∀[eq:Top]. ∀[r:CRng]. ∀[f,g:Top].  ((f*g)[{}] ~ (f[{}] * g[{}]) +r 0)
BY
{ (xxxAutoxxx THEN RepeatFor 3 (D 2) THEN DProdsAndUnions THEN RepeatFor 3 ((Computation THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[eq:Top].  \mforall{}[r:CRng].  \mforall{}[f,g:Top].    ((f*g)[\{\}]  \msim{}  (f[\{\}]  *  g[\{\}])  +r  0)


By

---

Latex:
(xxxAutoxxx  THEN  RepeatFor  3  (D  2)  THEN  DProdsAndUnions  THEN  RepeatFor  3  ((Computation  THEN  Auto)))

---

Home Index