---

Step * 2 of Lemma fun_exp-mul


1. T : Type
2. f : T ⟶ T
3. n : ℤ
4. 0 < n
5. ∀[m:ℕ]. ∀[x:T].  ((f^(n - 1) * m x) = (λx.(f^m x)^n - 1 x) ∈ T)
6. m : ℕ
7. x : T
⊢ (f^n * m x) = (λx.(f^m x)^n x) ∈ T
BY
{ Subst ⌜n * m ~ m + ((n - 1) * m)⌝ 0⋅ }

1
.....equality..... 
1. T : Type
2. f : T ⟶ T
3. n : ℤ
4. 0 < n
5. ∀[m:ℕ]. ∀[x:T].  ((f^(n - 1) * m x) = (λx.(f^m x)^n - 1 x) ∈ T)
6. m : ℕ
7. x : T
⊢ n * m ~ m + ((n - 1) * m)

2
1. T : Type
2. f : T ⟶ T
3. n : ℤ
4. 0 < n
5. ∀[m:ℕ]. ∀[x:T].  ((f^(n - 1) * m x) = (λx.(f^m x)^n - 1 x) ∈ T)
6. m : ℕ
7. x : T
⊢ (f^m + ((n - 1) * m) x) = (λx.(f^m x)^n x) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}[m:\mBbbN{}].  \mforall{}[x:T].    ((f\^{}(n  -  1)  *  m  x)  =  (\mlambda{}x.(f\^{}m  x)\^{}n  -  1  x))
6.  m  :  \mBbbN{}
7.  x  :  T
\mvdash{}  (f\^{}n  *  m  x)  =  (\mlambda{}x.(f\^{}m  x)\^{}n  x)


By

---

Latex:
Subst  \mkleeneopen{}n  *  m  \msim{}  m  +  ((n  -  1)  *  m)\mkleeneclose{}  0\mcdot{}

---

Home Index