---

Step * 1 of Lemma fps-compose-one


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. f : PowerSeries(X;r)
7. bs : bag(X)
8. bs = {} ∈ bag(X)
⊢ Σ(L∈bag-parts'(eq;bs;x)). if bag-null(hd(L) + bag-rep(||tl(L)||;x)) then 1 else 0 fi  * Πa ∈ tl(L). f a = 1 ∈ |r|
BY
{ xxx((FLemma `equal-empty-bag` [-1] THENA Auto) THEN HypSubst' -1 0 THEN FpsCompute 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  x  :  X
6.  f  :  PowerSeries(X;r)
7.  bs  :  bag(X)
8.  bs  =  \{\}
\mvdash{}  \mSigma{}(L\mmember{}bag-parts'(eq;bs;x)).  if  bag-null(hd(L)  +  bag-rep(||tl(L)||;x))  then  1  else  0  fi   
                                                        * 
                                                        \mPi{}a  \mmember{}  tl(L).  f  a
=  1


By

---

Latex:
xxx((FLemma  `equal-empty-bag`  [-1]  THENA  Auto)  THEN  HypSubst'  -1  0  THEN  FpsCompute  0  THEN  Auto)xxx

---

Home Index