for K being Field
for V1 being finite-dimensional VectSp of K holds
( V1 is trivial iff dim V1 = 0 )