let T, S be non empty TopSpace; :: thesis: ( the carrier of T = the carrier of S & the topology of T = the topology of S & T is injective implies S is injective )
assume that
A1: the carrier of T = the carrier of S and
A2: the topology of T = the topology of S and
A3: T is injective ; :: thesis: S is injective
A4: ( [#] S <> {} & [#] T <> {} ) ;
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for f being Function of X,S st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
let f be Function of X,S; :: thesis: ( f is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f ) )
assume A5: f is continuous ; :: thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
reconsider f' = f as Function of X,T by A1;
for P being Subset of T st P is open holds
f' " P is open

proof

let P be Subset of T; :: thesis: ( P is open implies f' " P is open )
assume A6: P is open ; :: thesis: f' " P is open
reconsider P' = P as Subset of S by A1;
P' in the topology of S by A2, A6, PRE_TOPC:def 5;
then P' is open by PRE_TOPC:def 5;
hence f' " P is open by A4, A5, TOPS_2:55; :: thesis: verum

end;

then A7: f' is continuous by A4, TOPS_2:55;
let Y be non empty TopSpace; :: thesis: ( X is SubSpace of Y implies ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f ) )
assume X is SubSpace of Y ; :: thesis: ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
then consider h being Function of Y,T such that
A8: h is continuous and
A9: h | the carrier of X = f' by A3, A7, Def5;
reconsider g = h as Function of Y,S by A1;
take g ; :: thesis: ( g is continuous & g | the carrier of X = f )
for P being Subset of S st P is open holds
g " P is open

proof

let P be Subset of S; :: thesis: ( P is open implies g " P is open )
assume A10: P is open ; :: thesis: g " P is open
reconsider P' = P as Subset of T by A1;
P' in the topology of T by A2, A10, PRE_TOPC:def 5;
then P' is open by PRE_TOPC:def 5;
hence g " P is open by A4, A8, TOPS_2:55; :: thesis: verum

end;

hence g is continuous by A4, TOPS_2:55; :: thesis: g | the carrier of X = f
thus g | the carrier of X = f by A9; :: thesis: verum