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;
A1: UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin A by RUSUB_3:def 2;
B' is linearly-independent by RUSUB_3:def 2;
then A2: card B' <= card A' by A1, Th2;
A3: UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin B by RUSUB_3:def 2;
A' is linearly-independent by RUSUB_3:def 2;
then card A' <= card B' by A3, Th2;
hence card A = card B by A2, XXREAL_0:1; :: thesis: verum