---

Step * 2 1 of Lemma flip_bijection


1. k : ℕ
2. i : ℕk
3. j : ℕk
4. ∀a1,a2:ℕk.  ((((i, j) a1) = ((i, j) a2) ∈ ℕk) ⇒ (a1 = a2 ∈ ℕk))
5. b : ℕk
⊢ ((i, j) ((i, j) b)) = b ∈ ℕk
BY
{ (RepUR ``flip`` 0 THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  i  :  \mBbbN{}k
3.  j  :  \mBbbN{}k
4.  \mforall{}a1,a2:\mBbbN{}k.    ((((i,  j)  a1)  =  ((i,  j)  a2))  {}\mRightarrow{}  (a1  =  a2))
5.  b  :  \mBbbN{}k
\mvdash{}  ((i,  j)  ((i,  j)  b))  =  b


By

---

Latex:
(RepUR  ``flip``  0  THEN  Repeat  (AutoSplit))

---

Home Index