let V be RealLinearSpace; :: thesis: ( V is finite-dimensional implies for A, B being Basis of V holds card A = card B )
assume A1: V is finite-dimensional ; :: thesis: for A, B being Basis of V holds card A = card B
let A, B be Basis of V; :: thesis: card A = card B
reconsider A9 = A, B9 = B as finite Subset of V by A1, Th23;
( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin B & A9 is linearly-independent ) by RLVECT_3:def 3;
then A2: card A9 <= card B9 by Th22;
( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B9 is linearly-independent ) by RLVECT_3:def 3;
then card B9 <= card A9 by Th22;
hence card A = card B by A2, XXREAL_0:1; :: thesis: verum