theorem Th6: :: RUSUB_4:6

for V being RealUnitarySpace holds (0). V is finite-dimensional