---

Step * of Lemma fps-ucont-composition

∀[X:Type]
  ∀eq:EqDecider(X). ∀r:CRng. ∀F,G:PowerSeries(X;r) ⟶ PowerSeries(X;r).
    (fps-ucont(X;eq;r;f.F[f]) ⇒ fps-ucont(X;eq;r;f.G[f]) ⇒ fps-ucont(X;eq;r;f.F o G[f])) 
  supposing valueall-type(X)
BY
{ (Auto THEN (D 0 THEN Auto) THEN (With ⌜b⌝ (D (-3))⋅ THEN Auto) THEN ExRepD THEN All (RepUR ``compose so_apply``)⋅) }

1
1. [X] : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. F : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
7. fps-ucont(X;eq;r;f.G f)
8. b : bag(X)
9. d : bag(X)
10. ∀f:PowerSeries(X;r). (F f[b] = F fps-restrict(eq;r;f;d)[b] ∈ |r|)
⊢ ∃d:bag(X). ∀f:PowerSeries(X;r). (F (G f)[b] = F (G fps-restrict(eq;r;f;d))[b] ∈ |r|)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}eq:EqDecider(X).  \mforall{}r:CRng.  \mforall{}F,G:PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r).
        (fps-ucont(X;eq;r;f.F[f])  {}\mRightarrow{}  fps-ucont(X;eq;r;f.G[f])  {}\mRightarrow{}  fps-ucont(X;eq;r;f.F  o  G[f])) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  (With  \mkleeneopen{}b\mkleeneclose{}  (D  (-3))\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  All  (RepUR  ``compose  so\_apply``)\mcdot{})

---

Home Index