---

Step * of Lemma vs-hom_wf

∀[K:CRng]. ∀[A,B:VectorSpace(K)].  (Hom(A;B) ∈ VectorSpace(K))
BY
{ (ProveWfLemma
   THEN (All (Unfold `vs-map`) THEN DSetVars THEN MemTypeCD THEN Reduce 0 THEN Auto)
   THEN (RWW "5 6 7 8 9 10 11 12 vs-mul-linear vs-mul-mul" 0 THENA Auto)
   THEN RW VSNormC 0
   THEN Auto
   THEN RW RngNormC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[A,B:VectorSpace(K)].    (Hom(A;B)  \mmember{}  VectorSpace(K))


By

---

Latex:
(ProveWfLemma
  THEN  (All  (Unfold  `vs-map`)  THEN  DSetVars  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)
  THEN  (RWW  "5  6  7  8  9  10  11  12  vs-mul-linear  vs-mul-mul"  0  THENA  Auto)
  THEN  RW  VSNormC  0
  THEN  Auto
  THEN  RW  RngNormC  0
  THEN  Auto)

---

Home Index