let GF be Field; :: thesis: for V being VectSp of GF holds (0). V is finite-dimensional
let V be VectSp of GF; :: thesis: (0). V is finite-dimensional
reconsider V9 = (0). V as strict VectSp of GF ;
reconsider I = {} the carrier of V9 as finite Subset of V9 ;
the carrier of V9 = {(0. V)} by VECTSP_4:def 3
.= {(0. V9)} by VECTSP_4:11
.= the carrier of ((0). V9) by VECTSP_4:def 3 ;
then A1: V9 = (0). V9 by VECTSP_4:31;
Lin I = (0). V9 by VECTSP_7:9;
then I is Basis of V9 by A1, VECTSP_7:def 3;
hence (0). V is finite-dimensional by MATRLIN:def 1; :: thesis: verum