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, T_0TOPSP:def 1;
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 9;
A7: p is one-to-one by A3, TOPS_2:72;
set F = (p " ) * f;
p " is continuous by A3, TOPS_2:def 5;
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, WAYBEL18:def 5;
take g = p * G; :: thesis: ( g is continuous & g | the carrier of X = f )
A10: rng p = [#] T by A3, TOPS_2:72;
A11: for x being set st x in dom f holds
g . x = f . x

proof

let x be set ; :: 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 5;
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:23
.= p . (((p " ) * f) . x) by A9, A12, FUNCT_1:72
.= p . ((p " ) . (f . x)) by A12, FUNCT_1:23
.= (p * (p " )) . (f . x) by A14, FUNCT_1:23
.= (id the carrier of T) . (f . x) by A10, A7, TOPS_2:65
.= f . x by A13, FUNCT_1:34 ;
:: thesis: verum

end;

p is continuous by A3, TOPS_2:def 5;
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:68; :: thesis: verum