let V be RealUnitarySpace; :: thesis: (0). V is finite-dimensional
reconsider V9 = (0). V as strict RealUnitarySpace ;
reconsider I = {} the carrier of V9 as finite Subset of V9 ;
the carrier of V9 = {(0. V)} by RUSUB_1:def 2
.= {(0. V9)} by RUSUB_1:4
.= the carrier of ((0). V9) by RUSUB_1:def 2 ;
then A1: V9 = (0). V9 by RUSUB_1:26;
( I is linearly-independent & Lin I = (0). V9 ) by RLVECT_3:7, RUSUB_3:3;
then I is Basis of V9 by A1, RUSUB_3:def 2;
hence (0). V is finite-dimensional ; :: thesis: verum