theorem Th3: :: RUSUB_4:3

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