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

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


Latex:


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


By


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




Home Index