set f = (id REAL) +* (NAT --> REAL);

reconsider X = (REAL \ NAT) \/ {REAL} as non empty set ;

A1: rng ((id REAL) +* (NAT --> REAL)) c= (REAL \ NAT) \/ {REAL} by Th15;

REAL \/ NAT = REAL by XBOOLE_1:12, NUMBERS:19;

then dom ((id REAL) +* (NAT --> REAL)) = the carrier of R^1 by Th14, TOPMETR:17;

then reconsider f = (id REAL) +* (NAT --> REAL) as Function of the carrier of R^1,X by A1, FUNCT_2:2;

set O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } ;

{ (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } c= bool X

( fA = f " A & fA is closed ) } as Subset-Family of X ;

set T = TopStruct(# X,O #);

reconsider f = f as Function of R^1,TopStruct(# X,O #) ;

A2: for A being Subset of TopStruct(# X,O #) holds

( A is closed iff f " A is closed )

take T ; :: thesis: ( the carrier of T = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,T st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) ) )

thus the carrier of T = (REAL \ NAT) \/ {REAL} ; :: thesis: ex f being Function of R^1,T st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) )

reconsider f = f as Function of R^1,T ;

take f ; :: thesis: ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) )

thus ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) ) by A2; :: thesis: verum

reconsider X = (REAL \ NAT) \/ {REAL} as non empty set ;

A1: rng ((id REAL) +* (NAT --> REAL)) c= (REAL \ NAT) \/ {REAL} by Th15;

REAL \/ NAT = REAL by XBOOLE_1:12, NUMBERS:19;

then dom ((id REAL) +* (NAT --> REAL)) = the carrier of R^1 by Th14, TOPMETR:17;

then reconsider f = (id REAL) +* (NAT --> REAL) as Function of the carrier of R^1,X by A1, FUNCT_2:2;

set O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } ;

{ (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } c= bool X

proof

then reconsider O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } or B in bool X )

assume B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } ; :: thesis: B in bool X

then ex A being Subset of X st

( B = X \ A & ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) ) ;

hence B in bool X ; :: thesis: verum

end;( fA = f " A & fA is closed ) } or B in bool X )

assume B in { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) } ; :: thesis: B in bool X

then ex A being Subset of X st

( B = X \ A & ex fA being Subset of R^1 st

( fA = f " A & fA is closed ) ) ;

hence B in bool X ; :: thesis: verum

( fA = f " A & fA is closed ) } as Subset-Family of X ;

set T = TopStruct(# X,O #);

reconsider f = f as Function of R^1,TopStruct(# X,O #) ;

A2: for A being Subset of TopStruct(# X,O #) holds

( A is closed iff f " A is closed )

proof

then reconsider T = TopStruct(# X,O #) as non empty strict TopSpace by Th6;
let A be Subset of TopStruct(# X,O #); :: thesis: ( A is closed iff f " A is closed )

thus ( A is closed implies f " A is closed ) :: thesis: ( f " A is closed implies A is closed )

then X \ A in O ;

then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def 2;

hence A is closed by PRE_TOPC:def 3; :: thesis: verum

end;thus ( A is closed implies f " A is closed ) :: thesis: ( f " A is closed implies A is closed )

proof

assume
f " A is closed
; :: thesis: A is closed
assume
A is closed
; :: thesis: f " A is closed

then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def 3;

then ([#] TopStruct(# X,O #)) \ A in the topology of TopStruct(# X,O #) by PRE_TOPC:def 2;

then consider B being Subset of X such that

A3: X \ B = ([#] TopStruct(# X,O #)) \ A and

A4: ex fA being Subset of R^1 st

( fA = f " B & fA is closed ) ;

B = ([#] TopStruct(# X,O #)) \ (([#] TopStruct(# X,O #)) \ A) by A3, PRE_TOPC:3;

hence f " A is closed by A4, PRE_TOPC:3; :: thesis: verum

end;then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def 3;

then ([#] TopStruct(# X,O #)) \ A in the topology of TopStruct(# X,O #) by PRE_TOPC:def 2;

then consider B being Subset of X such that

A3: X \ B = ([#] TopStruct(# X,O #)) \ A and

A4: ex fA being Subset of R^1 st

( fA = f " B & fA is closed ) ;

B = ([#] TopStruct(# X,O #)) \ (([#] TopStruct(# X,O #)) \ A) by A3, PRE_TOPC:3;

hence f " A is closed by A4, PRE_TOPC:3; :: thesis: verum

then X \ A in O ;

then ([#] TopStruct(# X,O #)) \ A is open by PRE_TOPC:def 2;

hence A is closed by PRE_TOPC:def 3; :: thesis: verum

take T ; :: thesis: ( the carrier of T = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,T st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) ) )

thus the carrier of T = (REAL \ NAT) \/ {REAL} ; :: thesis: ex f being Function of R^1,T st

( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) )

reconsider f = f as Function of R^1,T ;

take f ; :: thesis: ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) )

thus ( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of T holds

( A is closed iff f " A is closed ) ) ) by A2; :: thesis: verum