---

Step * of Lemma free-vs-maps-eq

∀[S:Type]. ∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[f,g:free-vs(K;S) ⟶ vs].
  f = g ∈ free-vs(K;S) ⟶ vs supposing ∀s:S. ((f <s>) = (g <s>) ∈ Point(vs))
BY
{ (InstLemma `free-vs-property` [] THEN RepeatFor 3 (ParallelLast') THEN Auto) }

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))
⊢ f = g ∈ free-vs(K;S) ⟶ vs

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:CRng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f,g:free-vs(K;S)  {}\mrightarrow{}  vs].
    f  =  g  supposing  \mforall{}s:S.  ((f  <s>)  =  (g  <s>))


By

---

Latex:
(InstLemma  `free-vs-property`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto)

---

Home Index