---

Step * 2 1 1 1 2 2 1 of Lemma free-vs-unique


1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. f : V ⟶ free-vs(K;S)
5. g : free-vs(K;S) ⟶ V
6. ∀a:Point(V). ((g (f a)) = a ∈ Point(V))
7. ∀b:Point(free-vs(K;S)). ((f (g b)) = b ∈ Point(free-vs(K;S)))
8. vs : VectorSpace(K)
9. f1 : S ⟶ Point(vs)
10. h : free-vs(K;S) ⟶ vs
11. ∀s:S. ((h <s>) = (f1 s) ∈ Point(vs))
12. ∀y:free-vs(K;S) ⟶ vs. ((∀s:S. ((y <s>) = (f1 s) ∈ Point(vs))) ⇒ (y = h ∈ free-vs(K;S) ⟶ vs))
13. y : V ⟶ vs
14. ∀s:S. ((y (g <s>)) = (f1 s) ∈ Point(vs))
⊢ y = (h o f) ∈ V ⟶ vs
BY
{ (InstHyp [⌜y o g⌝] (-3)⋅ THENA (Auto THEN Reduce 0 THEN Auto THEN BLemma `vs-map-compose` THEN Auto)) }

1
1. S : Type
2. K : CRng
3. V : VectorSpace(K)
4. f : V ⟶ free-vs(K;S)
5. g : free-vs(K;S) ⟶ V
6. ∀a:Point(V). ((g (f a)) = a ∈ Point(V))
7. ∀b:Point(free-vs(K;S)). ((f (g b)) = b ∈ Point(free-vs(K;S)))
8. vs : VectorSpace(K)
9. f1 : S ⟶ Point(vs)
10. h : free-vs(K;S) ⟶ vs
11. ∀s:S. ((h <s>) = (f1 s) ∈ Point(vs))
12. ∀y:free-vs(K;S) ⟶ vs. ((∀s:S. ((y <s>) = (f1 s) ∈ Point(vs))) ⇒ (y = h ∈ free-vs(K;S) ⟶ vs))
13. y : V ⟶ vs
14. ∀s:S. ((y (g <s>)) = (f1 s) ∈ Point(vs))
15. (y o g) = h ∈ free-vs(K;S) ⟶ vs
⊢ y = (h o f) ∈ V ⟶ vs

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  V  :  VectorSpace(K)
4.  f  :  V  {}\mrightarrow{}  free-vs(K;S)
5.  g  :  free-vs(K;S)  {}\mrightarrow{}  V
6.  \mforall{}a:Point(V).  ((g  (f  a))  =  a)
7.  \mforall{}b:Point(free-vs(K;S)).  ((f  (g  b))  =  b)
8.  vs  :  VectorSpace(K)
9.  f1  :  S  {}\mrightarrow{}  Point(vs)
10.  h  :  free-vs(K;S)  {}\mrightarrow{}  vs
11.  \mforall{}s:S.  ((h  <s>)  =  (f1  s))
12.  \mforall{}y:free-vs(K;S)  {}\mrightarrow{}  vs.  ((\mforall{}s:S.  ((y  <s>)  =  (f1  s)))  {}\mRightarrow{}  (y  =  h))
13.  y  :  V  {}\mrightarrow{}  vs
14.  \mforall{}s:S.  ((y  (g  <s>))  =  (f1  s))
\mvdash{}  y  =  (h  o  f)


By

---

Latex:
(InstHyp  [\mkleeneopen{}y  o  g\mkleeneclose{}]  (-3)\mcdot{}
  THENA  (Auto  THEN  Reduce  0  THEN  Auto  THEN  BLemma  `vs-map-compose`  THEN  Auto)
  )

---

Home Index