---

Step * 1 of Lemma fps-ucont-composition


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|)
BY
{ xxxAssert ⌜∃x:bag(X)
              ∀f:PowerSeries(X;r)
                (fps-restrict(eq;r;G f;d) = fps-restrict(eq;r;G fps-restrict(eq;r;f;x);d) ∈ PowerSeries(X;r))⌝⋅xxx }

1
.....assertion..... 
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|)
⊢ ∃x:bag(X)
   ∀f:PowerSeries(X;r). (fps-restrict(eq;r;G f;d) = fps-restrict(eq;r;G fps-restrict(eq;r;f;x);d) ∈ PowerSeries(X;r))

2
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|)
11. ∃x:bag(X)
     ∀f:PowerSeries(X;r). (fps-restrict(eq;r;G f;d) = fps-restrict(eq;r;G fps-restrict(eq;r;f;x);d) ∈ PowerSeries(X;r))
⊢ ∃d:bag(X). ∀f:PowerSeries(X;r). (F (G f)[b] = F (G fps-restrict(eq;r;f;d))[b] ∈ |r|)

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  F  :  PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)
6.  G  :  PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)
7.  fps-ucont(X;eq;r;f.G  f)
8.  b  :  bag(X)
9.  d  :  bag(X)
10.  \mforall{}f:PowerSeries(X;r).  (F  f[b]  =  F  fps-restrict(eq;r;f;d)[b])
\mvdash{}  \mexists{}d:bag(X).  \mforall{}f:PowerSeries(X;r).  (F  (G  f)[b]  =  F  (G  fps-restrict(eq;r;f;d))[b])


By

---

Latex:
xxxAssert  \mkleeneopen{}\mexists{}x:bag(X)
                        \mforall{}f:PowerSeries(X;r)
                            (fps-restrict(eq;r;G  f;d)  =  fps-restrict(eq;r;G  fps-restrict(eq;r;f;x);d))\mkleeneclose{}\mcdot{}xxx

---

Home Index