set V = the RealUnitarySpace;
take (0). the RealUnitarySpace ; :: thesis: ( (0). the RealUnitarySpace is strict & (0). the RealUnitarySpace is finite-dimensional )
thus (0). the RealUnitarySpace is strict ; :: thesis: (0). the RealUnitarySpace is finite-dimensional
take A = {} the carrier of ((0). the RealUnitarySpace); :: according to RUSUB_4:def 1 :: thesis: A is Basis of (0). the RealUnitarySpace
Lin A = (0). ((0). the RealUnitarySpace) by RUSUB_3:3;
then ( A is linearly-independent & Lin A = UNITSTR(# the carrier of ((0). the RealUnitarySpace), the ZeroF of ((0). the RealUnitarySpace), the addF of ((0). the RealUnitarySpace), the Mult of ((0). the RealUnitarySpace), the scalar of ((0). the RealUnitarySpace) #) ) by RLVECT_3:7, RUSUB_1:30;
hence A is Basis of (0). the RealUnitarySpace by RUSUB_3:def 2; :: thesis: verum