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