for GF being Field
for V being VectSp of GF st V is finite-dimensional holds
for A being Subset of V st A is linearly-independent holds
A is finite