---

Step * of Lemma nc-e'-comp-m

No Annotations
∀[I,J:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[j:{j:ℕ| ¬j ∈ J} ]. ∀[g:J ⟶ I]. ∀[k:{k:ℕ| ¬k ∈ I+i} ]. ∀[l:{l:ℕ| ¬l ∈ J+j} ].
  (g,i=j ⋅ m(j;l) = m(i;k) ⋅ g,i=j,k=l ∈ J+j+l ⟶ I+i)
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN (RWO "nh-comp-sq" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN (Unfold `nc-m` 0 THEN Reduce 0 THEN Fold `nc-m` 0)
   THEN RW (AddrC [2] (UnfoldC `nc-e\'`)) 0
   THEN (Reduce 0 THEN (Assert m(j;l) ∈ J+j+l ⟶ J+j BY Auto))
   THEN AutoSplit) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : {i:ℕ| ¬i ∈ I} 
4. j : {j:ℕ| ¬j ∈ J} 
5. g : J ⟶ I
6. k : {k:ℕ| ¬k ∈ I+i} 
7. l : {l:ℕ| ¬l ∈ J+j} 
8. x : names(I+i)
9. m(j;l) ∈ J+j+l ⟶ J+j
10. x = i ∈ ℤ
⊢ (dM-lift(J+j+l;J+j;m(j;l)) <j>) = (dM-lift(J+j+l;I+i+k;g,i=j,k=l) dMpair(i;k)) ∈ Point(dM(J+j+l))

2
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : {i:ℕ| ¬i ∈ I} 
4. j : {j:ℕ| ¬j ∈ J} 
5. g : J ⟶ I
6. k : {k:ℕ| ¬k ∈ I+i} 
7. l : {l:ℕ| ¬l ∈ J+j} 
8. x : names(I+i)
9. x ≠ i
10. m(j;l) ∈ J+j+l ⟶ J+j
⊢ (dM-lift(J+j+l;J+j;m(j;l)) (g x)) = (dM-lift(J+j+l;I+i+k;g,i=j,k=l) <x>) ∈ Point(dM(J+j+l))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  ].  \mforall{}[g:J  {}\mrightarrow{}  I].  \mforall{}[k:\{k:\mBbbN{}|  \mneg{}k  \mmember{}  I+i\}  ].
\mforall{}[l:\{l:\mBbbN{}|  \mneg{}l  \mmember{}  J+j\}  ].
    (g,i=j  \mcdot{}  m(j;l)  =  m(i;k)  \mcdot{}  g,i=j,k=l)


By

---

Latex:
(Auto
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  (RWO  "nh-comp-sq"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  (Unfold  `nc-m`  0  THEN  Reduce  0  THEN  Fold  `nc-m`  0)
  THEN  RW  (AddrC  [2]  (UnfoldC  `nc-e\mbackslash{}'`))  0
  THEN  (Reduce  0  THEN  (Assert  m(j;l)  \mmember{}  J+j+l  {}\mrightarrow{}  J+j  BY  Auto))
  THEN  AutoSplit)

---

Home Index