---

Step * of Lemma fps-add-ucont-general

∀[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[f]+G[f])))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (RepeatFor 2 ((D -3 With ⌜b⌝  THENA Auto)) THEN ExRepD)
   THEN (D 0 With ⌜d1 + d⌝  THEN Auto)
   THEN (Assert ∀X,Y:Top.  ((X+Y)[b] ~ X[b] +r Y[b]) BY
               (Auto THEN Computation))
   THEN RepeatFor 2 ((RWO "-1 -3 -5" 0 THENA Auto))
   THEN RepeatFor 3 (EqCDA)
   THEN (BLemma `fps-ext` THEN Auto)
   THEN RepUR ``fps-restrict fps-coeff`` 0⋅
   THEN RepeatFor 2 (AutoSplit)
   THEN D -2) }

1
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. sub-bag(X;b1;d1)
⊢ sub-bag(X;b1;d1 + d)

2
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. sub-bag(X;b1;d)
⊢ sub-bag(X;b1;d1 + d)

---

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[f]+G[f])))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (RepeatFor  2  ((D  -3  With  \mkleeneopen{}b\mkleeneclose{}    THENA  Auto))  THEN  ExRepD)
  THEN  (D  0  With  \mkleeneopen{}d1  +  d\mkleeneclose{}    THEN  Auto)
  THEN  (Assert  \mforall{}X,Y:Top.    ((X+Y)[b]  \msim{}  X[b]  +r  Y[b])  BY
                          (Auto  THEN  Computation))
  THEN  RepeatFor  2  ((RWO  "-1  -3  -5"  0  THENA  Auto))
  THEN  RepeatFor  3  (EqCDA)
  THEN  (BLemma  `fps-ext`  THEN  Auto)
  THEN  RepUR  ``fps-restrict  fps-coeff``  0\mcdot{}
  THEN  RepeatFor  2  (AutoSplit)
  THEN  D  -2)

---

Home Index