let X, Y be RealBanachSpace; :: thesis:
let T be Lipschitzian LinearOperator of X,Y; :: thesis:
assume A1: T is bijective ; :: thesis:
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:

let A be Subset of (LinearTopSpaceNorm X); :: thesis:
assume A5: A is open ; :: thesis:
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:

end;

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

end;

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

now :: thesis:

let x be Point of Y; :: thesis:
assume x in the carrier of Y ; :: thesis:
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:

end;

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