let X, Y be non empty strict TopSpace; :: thesis: ( the carrier of X = (REAL \ NAT) \/ {REAL} & 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 ) ) ) & the carrier of Y = (REAL \ NAT) \/ {REAL} & 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 ) ) ) implies X = Y )
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: X = Y
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

proof

let V be object ; :: according to TARSKI:def 3 :: thesis: ( not V in the topology of Y or V in the topology of X )
assume A14: V in the topology of Y ; :: thesis: V in the topology of X
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: verum

end;

the topology of X c= the topology of Y

proof

let V be object ; :: according to TARSKI:def 3 :: thesis: ( not V in the topology of X or V in the topology of Y )
assume A15: V in the topology of X ; :: thesis: V in the topology of Y
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: verum

end;

hence X = Y by A5, A7, A13, XBOOLE_0:def 10; :: thesis: verum