let X, Y be RealBanachSpace; :: thesis: for T being Lipschitzian LinearOperator of X,Y st T is bijective holds
T " is Lipschitzian LinearOperator of Y,X
let T be Lipschitzian LinearOperator of X,Y; :: thesis: ( T is bijective implies T " is Lipschitzian LinearOperator of Y,X )
assume A1: T is bijective ; :: thesis: T " is Lipschitzian LinearOperator of Y,X
A2: ( the carrier of (LinearTopSpaceNorm X) = the carrier of X & the carrier of (LinearTopSpaceNorm Y) = the carrier of Y ) by NORMSP_2:def 4;
then reconsider S = T as Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) ;
reconsider T2 = T " as LinearOperator of Y,X by Th1, A1;
reconsider T3 = T2 as Function of (LinearTopSpaceNorm Y),(LinearTopSpaceNorm X) by A2;
A3: T3 is continuous

proof

A4: ( [#] (LinearTopSpaceNorm Y) <> {} & [#] (LinearTopSpaceNorm X) <> {} ) ;

now :: thesis: for A being Subset of (LinearTopSpaceNorm X) st A is open holds
T3 " A is open

let A be Subset of (LinearTopSpaceNorm X); :: thesis: ( A is open implies T3 " A is open )
assume A5: A is open ; :: thesis: T3 " A is open
T3 " A = (T3 ") .: A by A1, FUNCT_1:85
.= S .: A by A1, FUNCT_1:43 ;
hence T3 " A is open by A5, A2, A1, LOPBAN_6:16, T_0TOPSP:def 2; :: thesis: verum

end;

hence T3 is continuous by A4, TOPS_2:43; :: thesis: verum

end;

A6: dom T2 = the carrier of Y by FUNCT_2:def 1;

now :: thesis: for x being Point of Y st x in the carrier of Y holds
T2 | the carrier of Y is_continuous_in x

let x be Point of Y; :: thesis: ( x in the carrier of Y implies T2 | the carrier of Y is_continuous_in x )
assume x in the carrier of Y ; :: thesis: T2 | the carrier of Y is_continuous_in x
reconsider xt = x as Point of (LinearTopSpaceNorm Y) by NORMSP_2:def 4;
A7: T3 is_continuous_at xt by A3, TMAP_1:44;
reconsider x1 = x as Point of (TopSpaceNorm Y) ;
reconsider T4 = T2 as Function of (TopSpaceNorm Y),(TopSpaceNorm X) ;
T4 is_continuous_at x1 by A7, NORMSP_2:35;
hence T2 | the carrier of Y is_continuous_in x by NORMSP_2:18; :: thesis: verum

end;

hence T " is Lipschitzian LinearOperator of Y,X by Th6, A6, NFCONT_1:def 7; :: thesis: verum