for K being Field
for V being finite-dimensional VectSp of K ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective