---

Step * 1 2 1 1 of Lemma restrict_perm_using_txpose


1. n : {1...}
2. p : Sym(n)
3. (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
⊢ p = id_perm() O p ∈ Sym(n)
BY
{ (RWH (GenLemmaC 2 `perm_ident`) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
3.  (txpose\_perm(n  -  1;p.f  (n  -  1))  O  p.f  (n  -  1))  =  (n  -  1)
\mvdash{}  p  =  id\_perm()  O  p


By

---

Latex:
(RWH  (GenLemmaC  2  `perm\_ident`)  0  THEN  Auto)

---

Home Index