let T, S be non empty TopSpace; :: thesis:
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:
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis:
let f be Function of X,S; :: thesis:
reconsider f9 = f as Function of X,T by A1;
A4: [#] S <> {} ;
assume A5: f is continuous ; :: thesis:
A6: for P being Subset of T st P is open holds
f9 " P is open

let P be Subset of T; :: thesis:
reconsider P9 = P as Subset of S by A1;
assume P is open ; :: thesis:
then P9 in the topology of S by A2;
then P9 is open ;
hence f9 " P is open by A4, A5, TOPS_2:43; :: thesis:

end;

let Y be non empty TopSpace; :: thesis:
assume A7: X is SubSpace of Y ; :: thesis:
A8: [#] T <> {} ;
then f9 is continuous by A6, TOPS_2:43;
then consider h being Function of Y,T such that
A9: h is continuous and
A10: h | the carrier of X = f9 by A3, A7;
reconsider g = h as Function of Y,S by A1;
take g ; :: thesis:
for P being Subset of S st P is open holds
g " P is open

let P be Subset of S; :: thesis:
reconsider P9 = P as Subset of T by A1;
assume P is open ; :: thesis:
then P9 in the topology of T by A2;
then P9 is open ;
hence g " P is open by A8, A9, TOPS_2:43; :: thesis:

end;