---

Step * 2 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^m + ((n - 1) * m) x) = (λx.(f^m x)^n x) ∈ T
BY
{ (RWO "fun_exp_add-sq" 0 THENA Auto) }

1
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 (f^(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\^{}m  +  ((n  -  1)  *  m)  x)  =  (\mlambda{}x.(f\^{}m  x)\^{}n  x)


By

---

Latex:
(RWO  "fun\_exp\_add-sq"  0  THENA  Auto)

---

Home Index