take V = 1 -VectSp_over K; :: thesis: ( not V is trivial & V is finite-dimensional )
dim V = 1 by MATRIX13:112;
then ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) by VECTSP_9:30;
hence ( not V is trivial & V is finite-dimensional ) ; :: thesis: verum