theorem Th16: :: RANKNULL:16
for F being Field
for V being finite-dimensional VectSp of F holds dim ((0). V) = 0