let X, Y be LinearTopSpace; :: thesis: for T being LinearOperator of X,Y

for S being Function of Y,X st T is bijective & T is open & S = T " holds

( S is LinearOperator of Y,X & S is onto & S is continuous )

let T be LinearOperator of X,Y; :: thesis: for S being Function of Y,X st T is bijective & T is open & S = T " holds

( S is LinearOperator of Y,X & S is onto & S is continuous )

let S be Function of Y,X; :: thesis: ( T is bijective & T is open & S = T " implies ( S is LinearOperator of Y,X & S is onto & S is continuous ) )

assume A1: ( T is bijective & T is open & S = T " ) ; :: thesis: ( S is LinearOperator of Y,X & S is onto & S is continuous )

then A2: ( T " is LinearOperator of Y,X & T " is one-to-one & rng (T ") = the carrier of X ) by Th1;

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

S is continuous

for S being Function of Y,X st T is bijective & T is open & S = T " holds

( S is LinearOperator of Y,X & S is onto & S is continuous )

let T be LinearOperator of X,Y; :: thesis: for S being Function of Y,X st T is bijective & T is open & S = T " holds

( S is LinearOperator of Y,X & S is onto & S is continuous )

let S be Function of Y,X; :: thesis: ( T is bijective & T is open & S = T " implies ( S is LinearOperator of Y,X & S is onto & S is continuous ) )

assume A1: ( T is bijective & T is open & S = T " ) ; :: thesis: ( S is LinearOperator of Y,X & S is onto & S is continuous )

then A2: ( T " is LinearOperator of Y,X & T " is one-to-one & rng (T ") = the carrier of X ) by Th1;

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

S is continuous

proof

end;

hence
( S is LinearOperator of Y,X & S is onto & S is continuous )
by A2, A1; :: thesis: verumnow :: thesis: for A being Subset of X st A is open holds

S " A is open

hence
S is continuous
by A3, TOPS_2:43; :: thesis: verumS " A is open

let A be Subset of X; :: thesis: ( A is open implies S " A is open )

assume A4: A is open ; :: thesis: S " A is open

S " A = (S ") .: A by A1, FUNCT_1:85

.= T .: A by A1, FUNCT_1:43 ;

hence S " A is open by A4, A1, T_0TOPSP:def 2; :: thesis: verum

end;assume A4: A is open ; :: thesis: S " A is open

S " A = (S ") .: A by A1, FUNCT_1:85

.= T .: A by A1, FUNCT_1:43 ;

hence S " A is open by A4, A1, T_0TOPSP:def 2; :: thesis: verum