---

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

.....assertion..... 
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
7. ∀s:S. ((h <s>) = (i s) ∈ Point(V))
8. f : V ⟶ free-vs(K;S)
9. ∀s:S. ((f (i s)) = <s> ∈ Point(free-vs(K;S)))
10. (f o h) = (λx.x) ∈ (Point(free-vs(K;S)) ⟶ Point(free-vs(K;S)))
11. h1 : V ⟶ V
12. ∀s:S. ((h1 (i s)) = (i s) ∈ Point(V))
13. ∀y:V ⟶ V. ((∀s:S. ((y (i s)) = (i s) ∈ Point(V))) ⇒ (y = h1 ∈ V ⟶ V))
14. (λx.x) = h1 ∈ V ⟶ V
⊢ (h o f) = h1 ∈ V ⟶ V
BY
{ BHyp -2 }

1
.....wf..... 
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
7. ∀s:S. ((h <s>) = (i s) ∈ Point(V))
8. f : V ⟶ free-vs(K;S)
9. ∀s:S. ((f (i s)) = <s> ∈ Point(free-vs(K;S)))
10. (f o h) = (λx.x) ∈ (Point(free-vs(K;S)) ⟶ Point(free-vs(K;S)))
11. h1 : V ⟶ V
12. ∀s:S. ((h1 (i s)) = (i s) ∈ Point(V))
13. ∀y:V ⟶ V. ((∀s:S. ((y (i s)) = (i s) ∈ Point(V))) ⇒ (y = h1 ∈ V ⟶ V))
14. (λx.x) = h1 ∈ V ⟶ V
⊢ h o f ∈ V ⟶ V

2
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
7. ∀s:S. ((h <s>) = (i s) ∈ Point(V))
8. f : V ⟶ free-vs(K;S)
9. ∀s:S. ((f (i s)) = <s> ∈ Point(free-vs(K;S)))
10. (f o h) = (λx.x) ∈ (Point(free-vs(K;S)) ⟶ Point(free-vs(K;S)))
11. h1 : V ⟶ V
12. ∀s:S. ((h1 (i s)) = (i s) ∈ Point(V))
13. ∀y:V ⟶ V. ((∀s:S. ((y (i s)) = (i s) ∈ Point(V))) ⇒ (y = h1 ∈ V ⟶ V))
14. (λx.x) = h1 ∈ V ⟶ V
⊢ ∀s:S. (((h o f) (i s)) = (i s) ∈ Point(V))

---

Latex:

---

Latex:
.....assertion..... 
1.  S  :  Type
2.  K  :  CRng
3.  V  :  VectorSpace(K)
4.  i  :  S  {}\mrightarrow{}  Point(V)
5.  \mforall{}vs:VectorSpace(K).  \mforall{}f:S  {}\mrightarrow{}  Point(vs).    \mexists{}!h:V  {}\mrightarrow{}  vs.  \mforall{}s:S.  ((h  (i  s))  =  (f  s))
6.  h  :  free-vs(K;S)  {}\mrightarrow{}  V
7.  \mforall{}s:S.  ((h  <s>)  =  (i  s))
8.  f  :  V  {}\mrightarrow{}  free-vs(K;S)
9.  \mforall{}s:S.  ((f  (i  s))  =  <s>)
10.  (f  o  h)  =  (\mlambda{}x.x)
11.  h1  :  V  {}\mrightarrow{}  V
12.  \mforall{}s:S.  ((h1  (i  s))  =  (i  s))
13.  \mforall{}y:V  {}\mrightarrow{}  V.  ((\mforall{}s:S.  ((y  (i  s))  =  (i  s)))  {}\mRightarrow{}  (y  =  h1))
14.  (\mlambda{}x.x)  =  h1
\mvdash{}  (h  o  f)  =  h1


By

---

Latex:
BHyp  -2

---

Home Index