---

Step * 1 1 1 of Lemma fps-ucont-composition


1. [X] : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. fps-ucont(X;eq;r;f.G f)
7. d : bag(X)
⊢ ∃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))
BY
{ xxx((Unfold `fps-ucont` (-2) THEN (Skolemize (-2) `h' THENA Auto)) THEN Thin (-4))xxx }

1
1. [X] : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. d : bag(X)
7. h : b:bag(X) ⟶ bag(X)
8. ∀b:bag(X). ∀f:PowerSeries(X;r).  (G f[b] = G fps-restrict(eq;r;f;h b)[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))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  G  :  PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)
6.  fps-ucont(X;eq;r;f.G  f)
7.  d  :  bag(X)
\mvdash{}  \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))


By

---

Latex:
xxx((Unfold  `fps-ucont`  (-2)  THEN  (Skolemize  (-2)  `h'  THENA  Auto))  THEN  Thin  (-4))xxx

---

Home Index