---

Step * of Lemma extend_permf_over_comp

No Annotations
∀n:ℕ. ∀f,g:ℕn ⟶ ℕn.  (extend_permf(g o f;n) = (extend_permf(g;n) o extend_permf(f;n)) ∈ (ℕn + 1 ⟶ ℕn + 1))
BY
{ (UnivCD THENA Auto) }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. g : ℕn ⟶ ℕn
⊢ extend_permf(g o f;n) = (extend_permf(g;n) o extend_permf(f;n)) ∈ (ℕn + 1 ⟶ ℕn + 1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.    (extend\_permf(g  o  f;n)  =  (extend\_permf(g;n)  o  extend\_permf(f;n)))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index