---

Step * 1 of Lemma dM-dM-homs-equal


1. I : fset(ℕ)
2. J : fset(ℕ)
3. h1 : dma-hom(dM(I);dM(J))
4. h2 : dma-hom(dM(I);dM(J))
5. ∀i:names(I). ((h1 <i>) = (h2 <i>) ∈ Point(dM(J)))
6. i : names(I)
7. (h1 <i>) = (h2 <i>) ∈ Point(dM(J))
⊢ (h1 <1-i>) = (h2 <1-i>) ∈ Point(dM(J))
BY
{ (DVar `h1'
   THEN DVar `h2'
   THEN (Assert ⌜(h1 ¬(<i>)) = (h2 ¬(<i>)) ∈ Point(dM(J))⌝⋅ THENA (RWO "4< 6<" 0 THEN Auto))
   THEN NthHypEq (-1)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  h1  :  dma-hom(dM(I);dM(J))
4.  h2  :  dma-hom(dM(I);dM(J))
5.  \mforall{}i:names(I).  ((h1  <i>)  =  (h2  <i>))
6.  i  :  names(I)
7.  (h1  <i>)  =  (h2  <i>)
\mvdash{}  (h1  ə-i>)  =  (h2  ə-i>)


By

---

Latex:
(DVar  `h1'
  THEN  DVar  `h2'
  THEN  (Assert  \mkleeneopen{}(h1  \mneg{}(<i>))  =  (h2  \mneg{}(<i>))\mkleeneclose{}\mcdot{}  THENA  (RWO  "4<  6<"  0  THEN  Auto))
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index