---

Step * 1 1 of Lemma all-vs-quotient-of-free


1. K : CRng
2. V : VectorSpace(K)
3. h : free-vs(K;Point(V)) ⟶ V
4. ∀s:Point(V). ((h <s>) = ((λx.x) s) ∈ Point(V))
5. ∀y:free-vs(K;Point(V)) ⟶ V. ((∀s:Point(V). ((y <s>) = ((λx.x) s) ∈ Point(V))) ⇒ (y = h ∈ free-vs(K;Point(V)) ⟶ V))
⊢ Surj(Point(free-vs(K;Point(V)));Point(V);h)
BY
{ (Reduce -2 THEN Unfold `surject` 0 THEN ParallelOp -2 THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  V  :  VectorSpace(K)
3.  h  :  free-vs(K;Point(V))  {}\mrightarrow{}  V
4.  \mforall{}s:Point(V).  ((h  <s>)  =  ((\mlambda{}x.x)  s))
5.  \mforall{}y:free-vs(K;Point(V))  {}\mrightarrow{}  V.  ((\mforall{}s:Point(V).  ((y  <s>)  =  ((\mlambda{}x.x)  s)))  {}\mRightarrow{}  (y  =  h))
\mvdash{}  Surj(Point(free-vs(K;Point(V)));Point(V);h)


By

---

Latex:
(Reduce  -2  THEN  Unfold  `surject`  0  THEN  ParallelOp  -2  THEN  Auto)

---

Home Index