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