theorem Th29: :: VECTSP_9:29

for GF being Field
for V being finite-dimensional VectSp of GF holds
( dim V = 0 iff (Omega). V = (0). V )