set V = the RealLinearSpace;
take (0). the RealLinearSpace ; :: thesis: ( (0). the RealLinearSpace is strict & (0). the RealLinearSpace is finite-dimensional )
thus (0). the RealLinearSpace is strict ; :: thesis: (0). the RealLinearSpace is finite-dimensional
take A = {} the carrier of ((0). the RealLinearSpace); :: according to RLVECT_5:def 1 :: thesis: A is Basis of (0). the RealLinearSpace
Lin A = (0). ((0). the RealLinearSpace) by RLVECT_3:16;
then ( A is linearly-independent & Lin A = RLSStruct(# the carrier of ((0). the RealLinearSpace), the ZeroF of ((0). the RealLinearSpace), the U5 of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace) #) ) by RLSUB_1:36, RLVECT_3:7;
hence A is Basis of (0). the RealLinearSpace by RLVECT_3:def 3; :: thesis: verum