---

Step * 1 1 of Lemma free-vs-maps-eq


1. S : Type
2. K : CRng
3. vs : VectorSpace(K)
4. ∀f:S ⟶ Point(vs). ∃!h:free-vs(K;S) ⟶ vs. ∀s:S. ((h <s>) = (f s) ∈ Point(vs))
5. f : free-vs(K;S) ⟶ vs
6. g : free-vs(K;S) ⟶ vs
7. ∀s:S. ((f <s>) = (g <s>) ∈ Point(vs))
8. h : free-vs(K;S) ⟶ vs
9. ∀s:S. ((h <s>) = (f <s>) ∈ Point(vs))
10. ∀y:free-vs(K;S) ⟶ vs. ((∀s:S. ((y <s>) = (f <s>) ∈ Point(vs))) ⇒ (y = h ∈ free-vs(K;S) ⟶ vs))
⊢ f = g ∈ free-vs(K;S) ⟶ vs
BY
{ ((InstHyp [⌜f⌝] (-1)⋅ THENA Auto) THEN InstHyp [⌜g⌝] (-2)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  vs  :  VectorSpace(K)
4.  \mforall{}f:S  {}\mrightarrow{}  Point(vs).  \mexists{}!h:free-vs(K;S)  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  <s>)  =  (f  s))
5.  f  :  free-vs(K;S)  {}\mrightarrow{}  vs
6.  g  :  free-vs(K;S)  {}\mrightarrow{}  vs
7.  \mforall{}s:S.  ((f  <s>)  =  (g  <s>))
8.  h  :  free-vs(K;S)  {}\mrightarrow{}  vs
9.  \mforall{}s:S.  ((h  <s>)  =  (f  <s>))
10.  \mforall{}y:free-vs(K;S)  {}\mrightarrow{}  vs.  ((\mforall{}s:S.  ((y  <s>)  =  (f  <s>)))  {}\mRightarrow{}  (y  =  h))
\mvdash{}  f  =  g


By

---

Latex:
((InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}g\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index