theorem Th1: :: LOPBAN_7:1

for X, Y being RealLinearSpace
for T being LinearOperator of X,Y st T is bijective holds
( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )