consider V being VectSp of K;
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 MATRLIN:def 3 :: thesis: A is Basis of (0). V
Lin A = (0). ((0). V) by VECTSP_7:14;
then Lin A = VectSpStr(# the carrier of ((0). V),the addF of ((0). V),the U2 of ((0). V),the lmult of ((0). V) #) by VECTSP_4:47;
hence A is Basis of (0). V by VECTSP_7:def 3; :: thesis: verum