for GF being 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