---

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


1. S : Type
2. s : S
3. K : CRng
4. ∀x,y:S.  (x = y ∈ S)
5. vs : VectorSpace(K)
6. f : S ⟶ Point(vs)
7. h : one-dim-vs(K) ⟶ vs
8. (h 1) = (f s) ∈ Point(vs)
9. ∀y:one-dim-vs(K) ⟶ vs. (((y 1) = (f s) ∈ Point(vs)) ⇒ (y = h ∈ one-dim-vs(K) ⟶ vs))
⊢ ∀y:one-dim-vs(K) ⟶ vs. ((∀s:S. ((y 1) = (f s) ∈ Point(vs))) ⇒ (y = h ∈ one-dim-vs(K) ⟶ vs))
BY
{ (RepeatFor 2 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  s  :  S
3.  K  :  CRng
4.  \mforall{}x,y:S.    (x  =  y)
5.  vs  :  VectorSpace(K)
6.  f  :  S  {}\mrightarrow{}  Point(vs)
7.  h  :  one-dim-vs(K)  {}\mrightarrow{}  vs
8.  (h  1)  =  (f  s)
9.  \mforall{}y:one-dim-vs(K)  {}\mrightarrow{}  vs.  (((y  1)  =  (f  s))  {}\mRightarrow{}  (y  =  h))
\mvdash{}  \mforall{}y:one-dim-vs(K)  {}\mrightarrow{}  vs.  ((\mforall{}s:S.  ((y  1)  =  (f  s)))  {}\mRightarrow{}  (y  =  h))


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index