theorem Th5: :: RUSUB_4:5
for V being RealUnitarySpace
for A, B being Basis of V st V is finite-dimensional holds
card A = card B