---

Step * of Lemma vs-mul-one

∀[K:RngSig]. ∀[vs:VectorSpace(K)]. ∀[x:Point(vs)].  (1 * x = x ∈ Point(vs))
BY
{ (Auto
   THEN (Assert vs ∈ VectorSpace(K) BY
               Auto)
   THEN (D 2 THEN Auto)
   THEN Unfolds ``vs-add vs-mul`` 0
   THEN MemTypeHD (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[x:Point(vs)].    (1  *  x  =  x)


By

---

Latex:
(Auto
  THEN  (Assert  vs  \mmember{}  VectorSpace(K)  BY
                          Auto)
  THEN  (D  2  THEN  Auto)
  THEN  Unfolds  ``vs-add  vs-mul``  0
  THEN  MemTypeHD  (-1)
  THEN  Auto)

---

Home Index