---

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

No Annotations
∀[I:fset(ℕ)]. (s ⋅ (new-name(I)1) = 1 ∈ I ⟶ I)
BY
{ (Auto THEN RWO "s-comp-nc-1" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  (s  \mcdot{}  (new-name(I)1)  =  1)


By

---

Latex:
(Auto  THEN  RWO  "s-comp-nc-1"  0  THEN  Auto)

---

Home Index