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 V' = (0). V as strict VectSp of GF ;
the carrier of V' = {(0. V)} by VECTSP_4:def 3
.= {(0. V')} by VECTSP_4:19
.= the carrier of ((0). V') by VECTSP_4:def 3 ;
then A1: V' = (0). V' by VECTSP_4:39;
reconsider I = {} the carrier of V' as finite Subset of V' ;
Lin I = (0). V' by VECTSP_7:14;
then I is Basis of V' by A1, VECTSP_7:def 3;
hence (0). V is finite-dimensional by MATRLIN:def 3; :: thesis: verum