---

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

∀K:CRng. ∀V:VectorSpace(K).
  ∃S:Type. ∃P:Point(free-vs(K;S)) ⟶ ℙ. (vs-subspace(K;free-vs(K;S);x.P[x]) ∧ V ≅ free-vs(K;S)//a.P[a])
BY
{ (Auto THEN (D 0 With ⌜Point(V)⌝  THENA Auto) THEN BLemma `implies-iso-vs-quotient` THEN Auto) }

1
1. K : CRng
2. V : VectorSpace(K)
⊢ ∃f:free-vs(K;Point(V)) ⟶ V. Surj(Point(free-vs(K;Point(V)));Point(V);f)

---

Latex:

---

Latex:
\mforall{}K:CRng.  \mforall{}V:VectorSpace(K).
    \mexists{}S:Type
      \mexists{}P:Point(free-vs(K;S))  {}\mrightarrow{}  \mBbbP{}.  (vs-subspace(K;free-vs(K;S);x.P[x])  \mwedge{}  V  \mcong{}  free-vs(K;S)//a.P[a])


By

---

Latex:
(Auto  THEN  (D  0  With  \mkleeneopen{}Point(V)\mkleeneclose{}    THENA  Auto)  THEN  BLemma  `implies-iso-vs-quotient`  THEN  Auto)

---

Home Index