let V be RealLinearSpace; :: thesis: (0). V is finite-dimensional

reconsider V9 = (0). V as strict RealLinearSpace ;

reconsider I = {} the carrier of V9 as finite Subset of V9 ;

the carrier of V9 = {(0. V)} by RLSUB_1:def 3

.= {(0. V9)} by RLSUB_1:11

.= the carrier of ((0). V9) by RLSUB_1:def 3 ;

then A1: V9 = (0). V9 by RLSUB_1:32;

( I is linearly-independent & Lin I = (0). V9 ) by RLVECT_3:7, RLVECT_3:16;

then I is Basis of V9 by A1, RLVECT_3:def 3;

hence (0). V is finite-dimensional ; :: thesis: verum

reconsider V9 = (0). V as strict RealLinearSpace ;

reconsider I = {} the carrier of V9 as finite Subset of V9 ;

the carrier of V9 = {(0. V)} by RLSUB_1:def 3

.= {(0. V9)} by RLSUB_1:11

.= the carrier of ((0). V9) by RLSUB_1:def 3 ;

then A1: V9 = (0). V9 by RLSUB_1:32;

( I is linearly-independent & Lin I = (0). V9 ) by RLVECT_3:7, RLVECT_3:16;

then I is Basis of V9 by A1, RLVECT_3:def 3;

hence (0). V is finite-dimensional ; :: thesis: verum