---

Step * of Lemma fps-mul-ucont

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[g:PowerSeries(X;r)].  fps-ucont(X;eq;r;f.(f*g)) supposing valueall-type(X)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN With ⌜b⌝ (D 0)⋅
   THEN Auto
   THEN RepUR ``fps-mul fps-coeff fps-restrict`` 0
   THEN BLemma `bag-summation-equal`
   THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. g : PowerSeries(X;r)
6. b : bag(X)
7. f : PowerSeries(X;r)
8. p : bag(X) × bag(X)
9. p ↓∈ bag-partitions(eq;b)
⊢ (* (f (fst(p))) (g (snd(p)))) = (* if deq-sub-bag(eq;fst(p);b) then f (fst(p)) else 0 fi  (g (snd(p)))) ∈ |r|

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. g : PowerSeries(X;r)
6. b : bag(X)
7. f : PowerSeries(X;r)
8. ∀p:bag(X) × bag(X)
     (p ↓∈ bag-partitions(eq;b)
     ⇒ ((* (f (fst(p))) (g (snd(p)))) = (* if deq-sub-bag(eq;fst(p);b) then f (fst(p)) else 0 fi  (g (snd(p)))) ∈ |r|))
⊢ IsMonoid(|r|;+r;0)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[g:PowerSeries(X;r)].    fps-ucont(X;eq;r;f.(f*g)) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  With  \mkleeneopen{}b\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RepUR  ``fps-mul  fps-coeff  fps-restrict``  0
  THEN  BLemma  `bag-summation-equal`
  THEN  Auto)

---

Home Index