---

Step * of Lemma fun_exp_add_sq_again

∀[n,m:ℕ]. ∀[f,i:Top].  (f^n + m i ~ f^n (f^m i))
BY
{ (InstLemma `fun_exp_add_sq` [] THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `fun\_exp\_add\_sq`  []  THEN  Trivial)

---

Home Index