---

Step * of Lemma flip-conjugation

∀[n:ℕ]. ∀[k:ℕn]. ∀[j:ℕk]. ∀[l:ℕn - k].  ((j, k + l) = ((k, k + l) o ((j, k) o (k, k + l))) ∈ (ℕn ⟶ ℕn))
BY
{ xxx(Auto THEN (Ext THENA Auto))xxx }

1
1. n : ℕ
2. k : ℕn
3. j : ℕk
4. l : ℕn - k
5. x : ℕn
⊢ ((j, k + l) x) = (((k, k + l) o ((j, k) o (k, k + l))) x) ∈ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}n].  \mforall{}[j:\mBbbN{}k].  \mforall{}[l:\mBbbN{}n  -  k].    ((j,  k  +  l)  =  ((k,  k  +  l)  o  ((j,  k)  o  (k,  k  +  l))))


By

---

Latex:
xxx(Auto  THEN  (Ext  THENA  Auto))xxx

---

Home Index