for V being RealUnitarySpace st V is finite-dimensional holds
for I being Basis of V holds I is finite