let GF be Field; 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; ( V is finite-dimensional implies for A, B being Basis of V holds card A = card B )
assume A1:
V is finite-dimensional
; for A, B being Basis of V holds card A = card B
let A, B be Basis of V; card A = card B
reconsider A9 = A, B9 = B as finite Subset of V by A1, Th20;
( ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin B & A9 is linearly-independent )
by VECTSP_7:def 3;
then A2:
card A9 <= card B9
by Th19;
( ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B9 is linearly-independent )
by VECTSP_7:def 3;
then
card B9 <= card A9
by Th19;
hence
card A = card B
by A2, XXREAL_0:1; verum