let V be RealLinearSpace; :: thesis: (0). V is finite-dimensional
reconsider V' = (0). V as strict RealLinearSpace ;
the carrier of V' = {(0. V)} by RLSUB_1:def 3
.= {(0. V')} by RLSUB_1:19
.= the carrier of ((0). V') by RLSUB_1:def 3 ;
then A1: V' = (0). V' by RLSUB_1:40;
reconsider I = {} the carrier of V' as finite Subset of V' ;
A2: I is linearly-independent by RLVECT_3:8;
Lin I = (0). V' by RLVECT_3:19;
then I is Basis of V' by A1, A2, RLVECT_3:def 3;
hence (0). V is finite-dimensional by Def1; :: thesis: verum