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

( 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

the topology of X c= the topology of Y
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;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

proof

hence
X = Y
by A5, A7, A13, XBOOLE_0:def 10; :: thesis: verum
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;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