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

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

A6:
dom T2 = the carrier of Y
by FUNCT_2:def 1;
A4:
( [#] (LinearTopSpaceNorm Y) <> {} & [#] (LinearTopSpaceNorm X) <> {} )
;

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

T3 " A is open

hence
T3 is continuous
by A4, TOPS_2:43; :: thesis: verumT3 " 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;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

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

hence
T " is Lipschitzian LinearOperator of Y,X
by Th6, A6, NFCONT_1:def 7; :: thesis: verumT2 | 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;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