lines (1. (K,n)) is Basis of (n -VectSp_over K) by Lm8;
hence n -VectSp_over K is finite-dimensional by MATRLIN:def 1; :: thesis: verum