---

Step * 1 1 of Lemma formal-sum-mul-add

.....wf..... 
1. S : Type
2. K : CRng
3. k : |K|
4. b : |K|
5. fs : basic-formal-sum(K;S)
⊢ {} ∈ basic-formal-sum(K;S)
BY
{ (Unfold `basic-formal-sum` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  S  :  Type
2.  K  :  CRng
3.  k  :  |K|
4.  b  :  |K|
5.  fs  :  basic-formal-sum(K;S)
\mvdash{}  \{\}  \mmember{}  basic-formal-sum(K;S)


By

---

Latex:
(Unfold  `basic-formal-sum`  0  THEN  Auto)

---

Home Index