---

Step * of Lemma vector-space_wf

∀K:RngSig. (VectorSpace(K) ∈ 𝕌')
BY
{ (Auto THEN Unfold `vector-space` 0 THEN Unfold `vs-point` 0 THEN RecordWf' THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:RngSig.  (VectorSpace(K)  \mmember{}  \mBbbU{}')


By

---

Latex:
(Auto  THEN  Unfold  `vector-space`  0  THEN  Unfold  `vs-point`  0  THEN  RecordWf'  THEN  Auto)

---

Home Index