---

Step * of Lemma fps-exp-add

No Annotations
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n,m:ℕ]. ∀[f:PowerSeries(X;r)].  ((f)^(n + m) = ((f)^(n)*(f)^(m)) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (InductionOnNat THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℤ
6. m : ℕ
7. f : PowerSeries(X;r)
⊢ (f)^(0 + m) = ((f)^(0)*(f)^(m)) ∈ PowerSeries(X;r)

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℤ
6. 0 < n
7. ∀[m:ℕ]. ∀[f:PowerSeries(X;r)].  ((f)^((n - 1) + m) = ((f)^(n - 1)*(f)^(m)) ∈ PowerSeries(X;r))
8. m : ℕ
9. f : PowerSeries(X;r)
⊢ (f)^(n + m) = ((f)^(n)*(f)^(m)) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[f:PowerSeries(X;r)].
        ((f)\^{}(n  +  m)  =  ((f)\^{}(n)*(f)\^{}(m))) 
    supposing  valueall-type(X)


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index