---

Step * 2 1 of Lemma fun_exp-mul

.....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)
BY
{ Auto }

---

Latex:

---

Latex:
.....equality..... 
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{}  n  *  m  \msim{}  m  +  ((n  -  1)  *  m)


By

---

Latex:
Auto

---

Home Index