lines M is Subset of (n -VectSp_over K) ;
hence M is FinSequence of (n -VectSp_over K) by FINSEQ_1:def 4; :: thesis: verum