for V being finite-dimensional RealLinearSpace
for W being RealLinearSpace st ex T being LinearOperator of V,W st T is bijective holds
( W is finite-dimensional & dim W = dim V )