let V be RealUnitarySpace; for A, B being Basis of V st V is finite-dimensional holds
card A = card B
let A, B be Basis of V; ( V is finite-dimensional implies card A = card B )
assume
V is finite-dimensional
; 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; verum