theorem Th7: :: RUSUB_4:7

for V being RealUnitarySpace
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional