consider V being RealUnitarySpace;
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 RUSUB_4:def 1 :: thesis: A is Basis of (0). V
Lin A = (0). ((0). V) by RUSUB_3:3;
then ( A is linearly-independent & Lin A = UNITSTR(# the carrier of ((0). V), the ZeroF of ((0). V), the addF of ((0). V), the Mult of ((0). V), the scalar of ((0). V) #) ) by RLVECT_3:8, RUSUB_1:30;
hence A is Basis of (0). V by RUSUB_3:def 2; :: thesis: verum