---

Step * 1 1 1 1 1 1 1 of Lemma vs-lift_wf-relative


1. K : CRng
2. vs : VectorSpace(K)
3. c : Point((x:vs | x = 0 ∈ Point(vs)))
⊢ c = 0 ∈ Point(vs)
BY
{ (RepUR ``vs-point sub-vs mk-vs`` -1 THEN Fold `vs-point` (-1) THEN D -1 THEN Trivial) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  vs  :  VectorSpace(K)
3.  c  :  Point((x:vs  |  x  =  0))
\mvdash{}  c  =  0


By

---

Latex:
(RepUR  ``vs-point  sub-vs  mk-vs``  -1  THEN  Fold  `vs-point`  (-1)  THEN  D  -1  THEN  Trivial)

---

Home Index