let GF be Field; :: thesis: for V being VectSp of GF st V is finite-dimensional holds
for A, B being Basis of V holds card A = card B
let V be VectSp of GF; :: 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 A' = A, B' = B as finite Subset of V by A1, Th24;
A2: VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) = Lin A by VECTSP_7:def 3;
B' is linearly-independent by VECTSP_7:def 3;
then A3: card B' <= card A' by A2, Th23;
A4: VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) = Lin B by VECTSP_7:def 3;
A' is linearly-independent by VECTSP_7:def 3;
then card A' <= card B' by A4, Th23;
hence card A = card B by A3, XXREAL_0:1; :: thesis: verum