---

Step * 1 2 of Lemma extend_perm_over_comp

.....set predicate..... 
1. n : ℕ
2. p : Sym(n)
3. q : Sym(n)
⊢ InvFuns(ℕn + 1;ℕn + 1;↑{n}(p
                              O q).f;↑{n}(p
                                           O q).b)
BY
{ (Assert ↑{n}(p O q) ∈ Sym(n + 1) THENA Auto{1,3}-1) }

1
1. n : ℕ
2. p : Sym(n)
3. q : Sym(n)
4. ↑{n}(p
         O q) ∈ Sym(n + 1)
⊢ InvFuns(ℕn + 1;ℕn + 1;↑{n}(p
                              O q).f;↑{n}(p
                                           O q).b)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  n  :  \mBbbN{}
2.  p  :  Sym(n)
3.  q  :  Sym(n)
\mvdash{}  InvFuns(\mBbbN{}n  +  1;\mBbbN{}n  +  1;\muparrow{}\{n\}(p
                                                            O  q).f;\muparrow{}\{n\}(p
                                                                                      O  q).b)


By

---

Latex:
(Assert  \muparrow{}\{n\}(p  O  q)  \mmember{}  Sym(n  +  1)  THENA  Auto\{1,3\}-1)

---

Home Index