---

Step * 2 1 of Lemma bijection_restriction


1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Surj(ℕk;ℕk;f)
5. ∀a1,a2:ℕk.  (((f a1) = (f a2) ∈ ℕk) ⇒ (a1 = a2 ∈ ℕk))
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. a1 : ℕk - 1
10. ∀a2:ℕk. (((f a1) = (f a2) ∈ ℕk) ⇒ (a1 = a2 ∈ ℕk))
⊢ ∀a2:ℕk - 1. (((f a1) = (f a2) ∈ ℕk - 1) ⇒ (a1 = a2 ∈ ℕk - 1))
BY
{ (RepeatFor 2 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k
3.  0  <  k
4.  Surj(\mBbbN{}k;\mBbbN{}k;f)
5.  \mforall{}a1,a2:\mBbbN{}k.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))
6.  (f  (k  -  1))  =  (k  -  1)
7.  f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1
8.  f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1
9.  a1  :  \mBbbN{}k  -  1
10.  \mforall{}a2:\mBbbN{}k.  (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))
\mvdash{}  \mforall{}a2:\mBbbN{}k  -  1.  (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index