---

Step * of Lemma fun_exp_add_sq

∀[n,m:ℕ]. ∀[f,i:Top].  (f^n + m i ~ f^n (f^m i))
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ ∀[m:ℕ]. ∀[f,i:Top].  (f^0 + m i ~ f^0 (f^m i))

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[f,i:Top].  (f^(n - 1) + m i ~ f^n - 1 (f^m i))
⊢ ∀[m:ℕ]. ∀[f,i:Top].  (f^n + m i ~ f^n (f^m i))

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[f,i:Top].    (f\^{}n  +  m  i  \msim{}  f\^{}n  (f\^{}m  i))


By

---

Latex:
InductionOnNat

---

Home Index