---

Step * 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))
⊢ f = g ∈ free-vs(K;S) ⟶ vs
BY
{ (((InstHyp [⌜λs.(f <s>)⌝] 4⋅ THENA Auto) THEN Reduce -1 THEN D -1) THEN ExRepD) }

1
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

---

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>))
\mvdash{}  f  =  g


By

---

Latex:
(((InstHyp  [\mkleeneopen{}\mlambda{}s.(f  <s>)\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  Reduce  -1  THEN  D  -1)  THEN  ExRepD)

---

Home Index