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
proof
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;
then reconsider O = { (X \ A) where A is Subset of X : ex fA being Subset of R^1 st
( 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
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 )
proof
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;
assume f " A is closed ; :: thesis: 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;
then reconsider T = TopStruct(# X,O #) as non empty strict TopSpace by Th6;
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