---

Step * 1 of Lemma flip_bijection


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

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  RepUR  ``flip``  0  THEN  Repeat  (AutoSplit))

---

Home Index