---

Step * 1 1 of Lemma fps-add-ucont-general


1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. F : PowerSeries(X;r) ⟶ PowerSeries(X;r)
5. G : PowerSeries(X;r) ⟶ PowerSeries(X;r)
6. b : bag(X)
7. d1 : bag(X)
8. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
9. d : bag(X)
10. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
11. f : PowerSeries(X;r)
12. ∀X,Y:Top.  ((X+Y)[b] ~ X[b] +r Y[b])
13. b1 : bag(X)
14. cs : bag(X)
15. d1 = (b1 + cs) ∈ bag(X)
⊢ sub-bag(X;b1;d1 + d)
BY
{ (D 0 With ⌜cs + d⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  eq  :  EqDecider(X)
3.  r  :  CRng
4.  F  :  PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)
5.  G  :  PowerSeries(X;r)  {}\mrightarrow{}  PowerSeries(X;r)
6.  b  :  bag(X)
7.  d1  :  bag(X)
8.  \mforall{}f:PowerSeries(X;r).  (F[f][b]  =  F[fps-restrict(eq;r;f;d1)][b])
9.  d  :  bag(X)
10.  \mforall{}f:PowerSeries(X;r).  (G[f][b]  =  G[fps-restrict(eq;r;f;d)][b])
11.  f  :  PowerSeries(X;r)
12.  \mforall{}X,Y:Top.    ((X+Y)[b]  \msim{}  X[b]  +r  Y[b])
13.  b1  :  bag(X)
14.  cs  :  bag(X)
15.  d1  =  (b1  +  cs)
\mvdash{}  sub-bag(X;b1;d1  +  d)


By

---

Latex:
(D  0  With  \mkleeneopen{}cs  +  d\mkleeneclose{}    THEN  Auto)

---

Home Index