Step
*
of Lemma
qv-mul_wf
∀[r:ℚ]. ∀[bs:ℚ List].  (qv-mul(r;bs) ∈ ℚ List)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[r:\mBbbQ{}].  \mforall{}[bs:\mBbbQ{}  List].    (qv-mul(r;bs)  \mmember{}  \mBbbQ{}  List)
By
Latex:
ProveWfLemma
Home
Index