---

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

.....subterm..... T:t
2:n
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|)
9. f : PowerSeries(X;r)
10. b : bag(X)
11. v : PowerSeries(X;r)
12. fps-restrict(eq;r;f;⋃b∈sub-bags(eq;d).h b) = v ∈ PowerSeries(X;r)
13. sub-bag(X;b;d)
⊢ fps-restrict(eq;r;f;h b) = fps-restrict(eq;r;v;h b) ∈ PowerSeries(X;r)
BY
{ xxx((BLemma `fps-ext` THEN Auto) THEN RepUR ``fps-restrict fps-coeff`` 0 THEN AutoSplit)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|)
9. f : PowerSeries(X;r)
10. b : bag(X)
11. v : PowerSeries(X;r)
12. fps-restrict(eq;r;f;⋃b∈sub-bags(eq;d).h b) = v ∈ PowerSeries(X;r)
13. sub-bag(X;b;d)
14. b1 : bag(X)
15. sub-bag(X;b1;h b)
⊢ (f b1) = (v b1) ∈ |r|

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  G  :  PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)
6.  d  :  bag(X)
7.  h  :  b:bag(X)  {}\mrightarrow{}  bag(X)
8.  \mforall{}b:bag(X).  \mforall{}f:PowerSeries(X;r).    (G  f[b]  =  G  fps-restrict(eq;r;f;h  b)[b])
9.  f  :  PowerSeries(X;r)
10.  b  :  bag(X)
11.  v  :  PowerSeries(X;r)
12.  fps-restrict(eq;r;f;\mcup{}b\mmember{}sub-bags(eq;d).h  b)  =  v
13.  sub-bag(X;b;d)
\mvdash{}  fps-restrict(eq;r;f;h  b)  =  fps-restrict(eq;r;v;h  b)


By

---

Latex:
xxx((BLemma  `fps-ext`  THEN  Auto)  THEN  RepUR  ``fps-restrict  fps-coeff``  0  THEN  AutoSplit)xxx

---

Home Index