theorem Th10: :: RUSUB_4:10

for V being finite-dimensional RealUnitarySpace holds dim V = dim ((Omega). V)