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 A9 = A, B9 = B as finite Subset of V by Th3;

( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin B & A9 is linearly-independent ) by RUSUB_3:def 2;

then A1: card A9 <= card B9 by Th2;

( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B9 is linearly-independent ) by RUSUB_3:def 2;

then card B9 <= card A9 by Th2;

hence card A = card B by A1, XXREAL_0:1; :: thesis: verum

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 A9 = A, B9 = B as finite Subset of V by Th3;

( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin B & A9 is linearly-independent ) by RUSUB_3:def 2;

then A1: card A9 <= card B9 by Th2;

( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B9 is linearly-independent ) by RUSUB_3:def 2;

then card B9 <= card A9 by Th2;

hence card A = card B by A1, XXREAL_0:1; :: thesis: verum