let X, Y be non empty strict TopSpace; :: thesis:
assume that
A5: the carrier of X = (REAL \ NAT) \/ {REAL} and
A6: ex f being Function of R^1,X st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of X holds
( A is closed iff f " A is closed ) ) ) and
A7: the carrier of Y = (REAL \ NAT) \/ {REAL} and
A8: ex f being Function of R^1,Y st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of Y holds
( A is closed iff f " A is closed ) ) ) ; :: thesis:
consider g being Function of R^1,Y such that
A9: g = (id REAL) +* (NAT --> REAL) and
A10: for A being Subset of Y holds
( A is closed iff g " A is closed ) by A8;
consider f being Function of R^1,X such that
A11: f = (id REAL) +* (NAT --> REAL) and
A12: for A being Subset of X holds
( A is closed iff f " A is closed ) by A6;
A13: the topology of Y c= the topology of X

let V be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: V in the topology of Y ; :: thesis:
then reconsider V1 = V as Subset of Y ;
reconsider V2 = V as Subset of X by A5, A7, A14;
reconsider V1 = V1 as Subset of Y ;
reconsider V2 = V2 as Subset of X ;
V1 is open by A14, PRE_TOPC:def 2;
then ([#] Y) \ V1 is closed by Lm2;
then f " (([#] Y) \ V1) is closed by A11, A9, A10;
then ([#] X) \ V2 is closed by A5, A7, A12;
then V2 is open by Lm2;
hence V in the topology of X by PRE_TOPC:def 2; :: thesis:

end;

let V be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: V in the topology of X ; :: thesis:
then reconsider V1 = V as Subset of X ;
reconsider V2 = V as Subset of Y by A5, A7, A15;
reconsider V1 = V1 as Subset of X ;
reconsider V2 = V2 as Subset of Y ;
V1 is open by A15, PRE_TOPC:def 2;
then ([#] X) \ V1 is closed by Lm2;
then g " (([#] X) \ V1) is closed by A11, A12, A9;
then ([#] Y) \ V2 is closed by A5, A7, A10;
then V2 is open by Lm2;
hence V in the topology of Y by PRE_TOPC:def 2; :: thesis:

end;