let V be RealLinearSpace; (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
; verum