set V = the VectSp of K;
take (0). the VectSp of K ; :: thesis: ( (0). the VectSp of K is strict & (0). the VectSp of K is finite-dimensional )
thus (0). the VectSp of K is strict ; :: thesis: (0). the VectSp of K is finite-dimensional
take A = {} the carrier of ((0). the VectSp of K); :: according to MATRLIN:def 1 :: thesis: A is Basis of ((0). the VectSp of K)
Lin A = (0). ((0). the VectSp of K) by VECTSP_7:9;
then Lin A = ModuleStr(# the carrier of ((0). the VectSp of K), the addF of ((0). the VectSp of K), the ZeroF of ((0). the VectSp of K), the lmult of ((0). the VectSp of K) #) by VECTSP_4:36;
hence A is Basis of ((0). the VectSp of K) by VECTSP_7:def 3; :: thesis: verum