Step
*
of Lemma
fps-compose-exp
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f:PowerSeries(X;r)]. ∀[n:ℕ].
((g)^(n)(x:=f) = (g(x:=f))^(n) ∈ PowerSeries(X;r))
supposing valueall-type(X)
BY
{ (InductionOnNat THEN RWW "fps-exp-zero fps-compose-one" 0 THEN Auto) }
1
.....upcase.....
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. n : ℤ
9. 0 < n
10. (g)^(n - 1)(x:=f) = (g(x:=f))^(n - 1) ∈ PowerSeries(X;r)
⊢ (g)^(n)(x:=f) = (g(x:=f))^(n) ∈ PowerSeries(X;r)
Latex:
Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)]. \mforall{}[r:CRng]. \mforall{}[x:X]. \mforall{}[g,f:PowerSeries(X;r)]. \mforall{}[n:\mBbbN{}].
((g)\^{}(n)(x:=f) = (g(x:=f))\^{}(n))
supposing valueall-type(X)
By
Latex:
(InductionOnNat THEN RWW "fps-exp-zero fps-compose-one" 0 THEN Auto)
Home
Index