---

Step * 1 of Lemma equipollent-non-zero


1. [T] : Type
2. n : ℕ+@i
3. f : T ⟶ ℕn@i
4. Inj(T;ℕn;f)@i
5. ∃a:T. ((f a) = 0 ∈ ℕn)@i
⊢ T
BY
{ ((D -1 THEN UseWitness ⌜a⌝⋅) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}\msupplus{}@i
3.  f  :  T  {}\mrightarrow{}  \mBbbN{}n@i
4.  Inj(T;\mBbbN{}n;f)@i
5.  \mexists{}a:T.  ((f  a)  =  0)@i
\mvdash{}  T


By

---

Latex:
((D  -1  THEN  UseWitness  \mkleeneopen{}a\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index