---

Step * 1 of Lemma fps-product-upto

.....equality..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
⊢ upto(k) ~ {0} + [1, k)
BY
{ RepUR ``upto bag-append single-bag`` 0⋅ }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. k : ℕ+
6. f : ℕk ⟶ PowerSeries(X;r)
⊢ [0, k) ~ [0 / [1, k)]

---

Latex:

---

Latex:
.....equality..... 
1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  k  :  \mBbbN{}\msupplus{}
6.  f  :  \mBbbN{}k  {}\mrightarrow{}  PowerSeries(X;r)
\mvdash{}  upto(k)  \msim{}  \{0\}  +  [1,  k)


By

---

Latex:
RepUR  ``upto  bag-append  single-bag``  0\mcdot{}

---

Home Index