for F being Field
for X, Y being VectSp of F
for T being linear-transformation of X,Y st T is bijective holds
( X is finite-dimensional iff Y is finite-dimensional )