---

Step * of Lemma relative-free-vs_wf

∀[K:CRng]. ∀[S,T:Type].  relative-free-vs(K;S;T) ∈ VectorSpace(K) supposing strong-subtype(T;S)
BY
{ (ProveWfLemma THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[K:CRng].  \mforall{}[S,T:Type].    relative-free-vs(K;S;T)  \mmember{}  VectorSpace(K)  supposing  strong-subtype(T;S)


By

---

Latex:
(ProveWfLemma  THEN  EAuto  1)

---

Home Index