---

Step * of Lemma s-comp-nc-0

∀[I:fset(ℕ)]. ∀[i:ℕ].  s ⋅ (i0) = 1 ∈ I ⟶ I supposing ¬i ∈ I
BY
{ (InstLemma  `nc-0-as-nc-p` [] THEN RepeatFor 2 (ParallelLast) THEN RWO "-1" 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    s  \mcdot{}  (i0)  =  1  supposing  \mneg{}i  \mmember{}  I


By

---

Latex:
(InstLemma    `nc-0-as-nc-p`  []  THEN  RepeatFor  2  (ParallelLast)  THEN  RWO  "-1"  0  THEN  EAuto  1)

---

Home Index