consider V being RealLinearSpace;
take (0). V ; :: thesis: ( (0). V is strict & (0). V is finite-dimensional )
thus (0). V is strict ; :: thesis: (0). V is finite-dimensional
take A = {} the carrier of ((0). V); :: according to RLVECT_5:def 1 :: thesis: A is Basis of (0). V
A1: A is linearly-independent by RLVECT_3:8;
Lin A = (0). ((0). V) by RLVECT_3:19;
then Lin A = RLSStruct(# the carrier of ((0). V),the U2 of ((0). V),the U5 of ((0). V),the Mult of ((0). V) #) by RLSUB_1:48;
hence A is Basis of (0). V by A1, RLVECT_3:def 3; :: thesis: verum