---

Step * 1 of Lemma nc-0-comp-s

.....truecase..... 
1. I : fset(ℕ)
2. K : fset(ℕ)
3. i : ℕ
4. f : K ⟶ I+i
5. (f i) = 0 ∈ Point(dM(K))
6. x : names(I+i)
7. x = i ∈ ℤ
⊢ (dM-lift(K;I+i;f) (dM-lift(I+i;I;s) {})) = (f x) ∈ Point(dM(K))
BY
{ (Subst' {} ~ 0 0 THENA Auto) }

1
1. I : fset(ℕ)
2. K : fset(ℕ)
3. i : ℕ
4. f : K ⟶ I+i
5. (f i) = 0 ∈ Point(dM(K))
6. x : names(I+i)
7. x = i ∈ ℤ
⊢ (dM-lift(K;I+i;f) (dM-lift(I+i;I;s) 0)) = (f x) ∈ Point(dM(K))

---

Latex:

---

Latex:
.....truecase..... 
1.  I  :  fset(\mBbbN{})
2.  K  :  fset(\mBbbN{})
3.  i  :  \mBbbN{}
4.  f  :  K  {}\mrightarrow{}  I+i
5.  (f  i)  =  0
6.  x  :  names(I+i)
7.  x  =  i
\mvdash{}  (dM-lift(K;I+i;f)  (dM-lift(I+i;I;s)  \{\}))  =  (f  x)


By

---

Latex:
(Subst'  \{\}  \msim{}  0  0  THENA  Auto)

---

Home Index