Step * of Lemma fun_exp_add_sq

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

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

2
.....upcase..... 
1. : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[f,i:Top].  (f^(n 1) f^n (f^m i))
⊢ ∀[m:ℕ]. ∀[f,i:Top].  (f^n 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