theorem Th85: :: REAL_NS2:85

for X, Y being RealLinearSpace
for L being LinearOperator of X,Y st L is bijective holds
ex K being LinearOperator of Y,X st
( K = L " & K is one-to-one & K is onto )