theorem Th32: :: RLVECT_5:32
for V being finite-dimensional RealLinearSpace holds
( dim V = 0 iff (Omega). V = (0). V )