let S, T be non empty TopSpace; :: thesis: ( S is injective & S,T are_homeomorphic implies T is injective )
assume that
A1: S is injective and
A2: S,T are_homeomorphic ; :: thesis: T is injective
consider p being Function of S,T such that
A3: p is being_homeomorphism by A2;
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for b₁ being Element of bool [: the carrier of X, the carrier of T:] holds
( not b₁ is continuous or for b₂ being TopStruct holds
( not X is SubSpace of b₂ or ex b₃ being Element of bool [: the carrier of b₂, the carrier of T:] st
( b₃ is continuous & b₃ | the carrier of X = b₁ ) ) )
let f be Function of X,T; :: thesis: ( not f is continuous or for b₁ being TopStruct holds
( not X is SubSpace of b₁ or ex b₂ being Element of bool [: the carrier of b₁, the carrier of T:] st
( b₂ is continuous & b₂ | the carrier of X = f ) ) )
assume A4: f is continuous ; :: thesis: for b₁ being TopStruct holds
( not X is SubSpace of b₁ or ex b₂ being Element of bool [: the carrier of b₁, the carrier of T:] st
( b₂ is continuous & b₂ | the carrier of X = f ) )
let Y be non empty TopSpace; :: thesis: ( not X is SubSpace of Y or ex b₁ being Element of bool [: the carrier of Y, the carrier of T:] st
( b₁ is continuous & b₁ | the carrier of X = f ) )
assume A5: X is SubSpace of Y ; :: thesis: ex b₁ being Element of bool [: the carrier of Y, the carrier of T:] st
( b₁ is continuous & b₁ | the carrier of X = f )
then A6: [#] X c= [#] Y by PRE_TOPC:def 4;
A7: p is one-to-one by A3;
set F = (p ") * f;
p " is continuous by A3;
then consider G being Function of Y,S such that
A8: G is continuous and
A9: G | the carrier of X = (p ") * f by A1, A4, A5;
take g = p * G; :: thesis: ( g is continuous & g | the carrier of X = f )
A10: rng p = [#] T by A3;
A11: for x being object st x in dom f holds
g . x = f . x

proof

let x be object ; :: thesis: ( x in dom f implies g . x = f . x )
assume A12: x in dom f ; :: thesis: g . x = f . x
then A13: f . x in rng f by FUNCT_1:def 3;
then f . x in the carrier of T ;
then A14: f . x in dom (p ") by FUNCT_2:def 1;
x in the carrier of X by A12;
then x in the carrier of Y by A6;
then x in dom G by FUNCT_2:def 1;
hence g . x = p . (G . x) by FUNCT_1:13
.= p . (((p ") * f) . x) by A9, A12, FUNCT_1:49
.= p . ((p ") . (f . x)) by A12, FUNCT_1:13
.= (p * (p ")) . (f . x) by A14, FUNCT_1:13
.= (id the carrier of T) . (f . x) by A10, A7, TOPS_2:52
.= f . x by A13, FUNCT_1:17 ;
:: thesis: verum

end;

p is continuous by A3;
hence g is continuous by A8; :: thesis: g | the carrier of X = f
dom f = the carrier of X by FUNCT_2:def 1
.= the carrier of Y /\ the carrier of X by A6, XBOOLE_1:28
.= (dom g) /\ the carrier of X by FUNCT_2:def 1 ;
hence g | the carrier of X = f by A11, FUNCT_1:46; :: thesis: verum