---

Step * 1 of Lemma fps-linear-ucont-equal


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. ∀f,g:PowerSeries(X;r).  (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r).  (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r).  (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r).  (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
⊢ F[fps-restrict(eq;r;f;d1)][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|
BY
{ xxxAssert ⌜F[fps-restrict(eq;r;f;d1 + d)][b] = G[fps-restrict(eq;r;f;d1 + d)][b] ∈ |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. ∀f,g:PowerSeries(X;r).  (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r).  (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r).  (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r).  (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
⊢ F[fps-restrict(eq;r;f;d1 + d)][b] = G[fps-restrict(eq;r;f;d1 + d)][b] ∈ |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. ∀f,g:PowerSeries(X;r).  (F[(f+g)] = (F[f]+F[g]) ∈ PowerSeries(X;r))
8. ∀f,g:PowerSeries(X;r).  (G[(f+g)] = (G[f]+G[g]) ∈ PowerSeries(X;r))
9. ∀c:|r|. ∀f:PowerSeries(X;r).  (F[(c)*f] = (c)*F[f] ∈ PowerSeries(X;r))
10. ∀c:|r|. ∀f:PowerSeries(X;r).  (G[(c)*f] = (c)*G[f] ∈ PowerSeries(X;r))
11. ∀b:bag(X). (F[<b>] = G[<b>] ∈ PowerSeries(X;r))
12. f : PowerSeries(X;r)
13. b : bag(X)
14. d1 : bag(X)
15. ∀f:PowerSeries(X;r). (F[f][b] = F[fps-restrict(eq;r;f;d1)][b] ∈ |r|)
16. d : bag(X)
17. ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
18. F[fps-restrict(eq;r;f;d1 + d)][b] = G[fps-restrict(eq;r;f;d1 + d)][b] ∈ |r|
⊢ F[fps-restrict(eq;r;f;d1)][b] = 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.  \mforall{}f,g:PowerSeries(X;r).    (F[(f+g)]  =  (F[f]+F[g]))
8.  \mforall{}f,g:PowerSeries(X;r).    (G[(f+g)]  =  (G[f]+G[g]))
9.  \mforall{}c:|r|.  \mforall{}f:PowerSeries(X;r).    (F[(c)*f]  =  (c)*F[f])
10.  \mforall{}c:|r|.  \mforall{}f:PowerSeries(X;r).    (G[(c)*f]  =  (c)*G[f])
11.  \mforall{}b:bag(X).  (F[<b>]  =  G[<b>])
12.  f  :  PowerSeries(X;r)
13.  b  :  bag(X)
14.  d1  :  bag(X)
15.  \mforall{}f:PowerSeries(X;r).  (F[f][b]  =  F[fps-restrict(eq;r;f;d1)][b])
16.  d  :  bag(X)
17.  \mforall{}f:PowerSeries(X;r).  (G[f][b]  =  G[fps-restrict(eq;r;f;d)][b])
\mvdash{}  F[fps-restrict(eq;r;f;d1)][b]  =  G[fps-restrict(eq;r;f;d)][b]


By

---

Latex:
xxxAssert  \mkleeneopen{}F[fps-restrict(eq;r;f;d1  +  d)][b]  =  G[fps-restrict(eq;r;f;d1  +  d)][b]\mkleeneclose{}\mcdot{}xxx

---

Home Index