---

Step * 2 of Lemma fps-mul-ucont


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)
BY
{ xxx(RepeatFor 2 (DVar `r') THEN Auto)xxx }

---

Latex:

---

Latex:

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.  \mforall{}p:bag(X)  \mtimes{}  bag(X)
          (p  \mdownarrow{}\mmember{}  bag-partitions(eq;b)
          {}\mRightarrow{}  ((*  (f  (fst(p)))  (g  (snd(p))))
                =  (*  if  deq-sub-bag(eq;fst(p);b)  then  f  (fst(p))  else  0  fi    (g  (snd(p))))))
\mvdash{}  IsMonoid(|r|;+r;0)


By

---

Latex:
xxx(RepeatFor  2  (DVar  `r')  THEN  Auto)xxx

---

Home Index