---

Step * 1 2 2 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|)
18. F[fps-restrict(eq;r;fps-restrict(eq;r;f;d1 + d);d1)][b]
= G[fps-restrict(eq;r;fps-restrict(eq;r;f;d1 + d);d)][b]
∈ |r|
19. b1 : bag(X)
20. ¬sub-bag(X;b1;d1 + d)
21. sub-bag(X;b1;d)
⊢ (f b1) = 0 ∈ |r|
BY
{ xxx(xxx(Assert sub-bag(X;d;d1 + d) BY (With ⌜d1⌝ (D 0)⋅ THEN Auto))xxx THEN RelRST THEN Auto)xxx }

---

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])
18.  F[fps-restrict(eq;r;fps-restrict(eq;r;f;d1  +  d);d1)][b]
=  G[fps-restrict(eq;r;fps-restrict(eq;r;f;d1  +  d);d)][b]
19.  b1  :  bag(X)
20.  \mneg{}sub-bag(X;b1;d1  +  d)
21.  sub-bag(X;b1;d)
\mvdash{}  (f  b1)  =  0


By

---

Latex:
xxx(xxx(Assert  sub-bag(X;d;d1  +  d)  BY  (With  \mkleeneopen{}d1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))xxx  THEN  RelRST  THEN  Auto)xxx

---

Home Index