---

Step * 1 of Lemma free-vs-unique


1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. ∃i:S ⟶ Point(V). ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) = (f s) ∈ Point(vs))
⊢ V ≅ free-vs(K;S)
BY
{ (ExRepD THEN (InstLemma `free-vs-property` [⌜S⌝;⌜K⌝;⌜V⌝;⌜i⌝]⋅ THENA Auto)) }

1
1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. i : S ⟶ Point(V)
5. ∀vs:VectorSpace(K). ∀f:S ⟶ Point(vs).  ∃!h:V ⟶ vs. ∀s:S. ((h (i s)) = (f s) ∈ Point(vs))
6. ∃!h:free-vs(K;S) ⟶ V. ∀s:S. ((h <s>) = (i s) ∈ Point(V))
⊢ V ≅ free-vs(K;S)

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  V  :  VectorSpace(K)
4.  \mexists{}i:S  {}\mrightarrow{}  Point(V).  \mforall{}vs:VectorSpace(K).  \mforall{}f:S  {}\mrightarrow{}  Point(vs).    \mexists{}!h:V  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  (i  s))  =  (f  s))
\mvdash{}  V  \mcong{}  free-vs(K;S)


By

---

Latex:
(ExRepD  THEN  (InstLemma  `free-vs-property`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index