---

Step * 1 of Lemma fps-single-bag-rep


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. n : ℤ
⊢ <{}> = 1 ∈ PowerSeries(X;r)
BY
{ (BLemma `fps-ext`  THEN Auto THEN RepUR ``fps-coeff fps-single fps-one`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  x  :  X
6.  n  :  \mBbbZ{}
\mvdash{}  <\{\}>  =  1


By

---

Latex:
(BLemma  `fps-ext`    THEN  Auto  THEN  RepUR  ``fps-coeff  fps-single  fps-one``  0  THEN  AutoSplit)

---

Home Index