---

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


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))
BY
{ HypSubst' (-1) 0⋅ }

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 i) ∈ Point(dM(K))

---

Latex:

---

Latex:

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)  0))  =  (f  x)


By

---

Latex:
HypSubst'  (-1)  0\mcdot{}

---

Home Index