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;
A4: p is continuous by A3, TOPS_2:def 5;
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 A5: 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 A6: 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 )
set F = (p " ) * f;
p " is continuous by A3, TOPS_2:def 5;
then (p " ) * f is continuous by A5;
then consider G being Function of Y,S such that
A7: G is continuous and
A8: G | the carrier of X = (p " ) * f by A1, A6, WAYBEL18:def 5;
take g = p * G; :: thesis: ( g is continuous & g | the carrier of X = f )
thus g is continuous by A4, A7; :: thesis: g | the carrier of X = f
A9: [#] X c= [#] Y by A6, PRE_TOPC:def 9;
A10: ( rng p = [#] T & p is one-to-one ) by A3, TOPS_2:72;
A11: dom f = the carrier of X by FUNCT_2:def 1
.= the carrier of Y /\ the carrier of X by A9, XBOOLE_1:28
.= (dom g) /\ the carrier of X by FUNCT_2:def 1 ;
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 x in the carrier of X ;
then x in the carrier of Y by A9;
then A13: x in dom G by FUNCT_2:def 1;
A14: f . x in rng f by A12, FUNCT_1:def 5;
then f . x in the carrier of T ;
then A15: f . x in dom (p " ) by FUNCT_2:def 1;
thus g . x = p . (G . x) by A13, FUNCT_1:23
.= p . (((p " ) * f) . x) by A8, A12, FUNCT_1:72
.= p . ((p " ) . (f . x)) by A12, FUNCT_1:23
.= (p * (p " )) . (f . x) by A15, FUNCT_1:23
.= (id the carrier of T) . (f . x) by A10, TOPS_2:65
.= f . x by A14, FUNCT_1:34 ; :: thesis: verum

end;

hence g | the carrier of X = f by A11, FUNCT_1:68; :: thesis: verum