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