for V being RealLinearSpace st V is finite-dimensional holds
for A, B being Basis of V holds card A = card B