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
proof
now :: thesis: for A being Subset of X st A is open holds
S " 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;
hence S is continuous by A3, TOPS_2:43; :: thesis: verum
end;
hence ( S is LinearOperator of Y,X & S is onto & S is continuous ) by A2, A1; :: thesis: verum