---

Step * 1 1 1 1 1 of Lemma sub-free-dim-1


1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. ∀x,y:T.  (x = y ∈ T)
6. s : T
7. b : basic-formal-sum(K;S)
8. bfs-predicate(K;S;p.snd(p) ∈ T;b)
9. ∀p:|K| × S. (p ↓∈ b ⇒ ((snd(p)) = s ∈ S))
⊢ b = {<Σ(p∈b). fst(p), s>} ∈ formal-sum(K;S)
BY
{ ((MoveToConcl (-1) THEN (GenConcl ⌜s = a ∈ S⌝⋅ THENA Auto)) THEN All Thin THEN (D 0 THENA Auto)) }

1
1. K : CRng
2. S : Type
3. b : basic-formal-sum(K;S)
4. a : S
5. ∀p:|K| × S. (p ↓∈ b ⇒ ((snd(p)) = a ∈ S))
⊢ b = {<Σ(p∈b). fst(p), a>} ∈ formal-sum(K;S)

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  T  :  Type
4.  strong-subtype(T;S)
5.  \mforall{}x,y:T.    (x  =  y)
6.  s  :  T
7.  b  :  basic-formal-sum(K;S)
8.  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;b)
9.  \mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  ((snd(p))  =  s))
\mvdash{}  b  =  \{<\mSigma{}(p\mmember{}b).  fst(p),  s>\}


By

---

Latex:
((MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}s  =  a\mkleeneclose{}\mcdot{}  THENA  Auto))  THEN  All  Thin  THEN  (D  0  THENA  Auto))

---

Home Index