let V be RealUnitarySpace; :: thesis: for A, B being Basis of V st V is finite-dimensional holds
card A = card B
let A, B be Basis of V; :: thesis: ( V is finite-dimensional implies card A = card B )
assume V is finite-dimensional ; :: thesis: card A = card B
then reconsider A' = A, B' = B as finite Subset of V by Th3;
( UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin B & A' is linearly-independent ) by RUSUB_3:def 2;
then A1: card A' <= card B' by Th2;
( UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin A & B' is linearly-independent ) by RUSUB_3:def 2;
then card B' <= card A' by Th2;
hence card A = card B by A1, XXREAL_0:1; :: thesis: verum