---

Step * of Lemma nh-comp-nc-m-eq

∀[I,K:fset(ℕ)]. ∀[i,j:ℕ]. ∀[f:K ⟶ I+i+j].  (i0) ⋅ s ⋅ s ⋅ f = m(i;j) ⋅ f ∈ K ⟶ I+i supposing (f i) = 0 ∈ Point(dM(K))
BY
{ (RepeatFor 5 ((Intro THENA Auto))
   THEN (Assert i ∈ names(I+i) BY
               (MemTypeCD THEN EAuto 1))
   THEN (Assert j ∈ names(I+i+j) BY
               (MemTypeCD THEN EAuto 1))
   THEN (Assert i ∈ names(I+i+j) BY
               (MemTypeCD THEN EAuto 1 THEN (MemTypeHD (-2) THENA Auto) THEN (Unhide THEN Auto) THEN EAuto 1))
   THEN (D 0 THENA Auto)
   THEN Unfold `names-hom` 0
   THEN (FunExt  THENA Auto)) }

1
1. I : fset(ℕ)
2. K : fset(ℕ)
3. i : ℕ
4. j : ℕ
5. f : K ⟶ I+i+j
6. i ∈ names(I+i)
7. j ∈ names(I+i+j)
8. i ∈ names(I+i+j)
9. (f i) = 0 ∈ Point(dM(K))
10. x : names(I+i)
⊢ ((i0) ⋅ s ⋅ s ⋅ f x) = (m(i;j) ⋅ f x) ∈ Point(dM(K))

---

Latex:

---

Latex:
\mforall{}[I,K:fset(\mBbbN{})].  \mforall{}[i,j:\mBbbN{}].  \mforall{}[f:K  {}\mrightarrow{}  I+i+j].    (i0)  \mcdot{}  s  \mcdot{}  s  \mcdot{}  f  =  m(i;j)  \mcdot{}  f  supposing  (f  i)  =  0


By

---

Latex:
(RepeatFor  5  ((Intro  THENA  Auto))
  THEN  (Assert  i  \mmember{}  names(I+i)  BY
                          (MemTypeCD  THEN  EAuto  1))
  THEN  (Assert  j  \mmember{}  names(I+i+j)  BY
                          (MemTypeCD  THEN  EAuto  1))
  THEN  (Assert  i  \mmember{}  names(I+i+j)  BY
                          (MemTypeCD
                            THEN  EAuto  1
                            THEN  (MemTypeHD  (-2)  THENA  Auto)
                            THEN  (Unhide  THEN  Auto)
                            THEN  EAuto  1))
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt    THENA  Auto))

---

Home Index