for X, Y being RealLinearSpace
for L being LinearOperator of X,Y st L is isomorphism holds
ex K being LinearOperator of Y,X st
( K = L " & K is isomorphism )