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
Lin A = (0). ((0). V) by RLVECT_3:19;
then ( A is linearly-independent & Lin A = RLSStruct(# the carrier of ((0). V), the ZeroF of ((0). V), the U5 of ((0). V), the Mult of ((0). V) #) ) by RLSUB_1:48, RLVECT_3:8;
hence A is Basis of (0). V by RLVECT_3:def 3; :: thesis: verum