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