---

Step * 2 1 1 2 1 of Lemma fun_exp_add_sq


1. n : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[f,i:Top].  (f^(n - 1) + m i ~ f^n - 1 (f^m i))
4. m : ℕ
5. f : Top
6. i : Top
7. ∀n:ℕ. ∀x:Top.  (f^n + 1 x ~ f (f^n x))
⊢ f (f^(n - 1) + m i) ~ f (f^n - 1 (f^m i))
BY
{ ((RW (SweepDnC (HypC 3)) 0) THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[m:\mBbbN{}].  \mforall{}[f,i:Top].    (f\^{}(n  -  1)  +  m  i  \msim{}  f\^{}n  -  1  (f\^{}m  i))
4.  m  :  \mBbbN{}
5.  f  :  Top
6.  i  :  Top
7.  \mforall{}n:\mBbbN{}.  \mforall{}x:Top.    (f\^{}n  +  1  x  \msim{}  f  (f\^{}n  x))
\mvdash{}  f  (f\^{}(n  -  1)  +  m  i)  \msim{}  f  (f\^{}n  -  1  (f\^{}m  i))


By

---

Latex:
((RW  (SweepDnC  (HypC  3))  0)  THEN  Auto')

---

Home Index