:: T_1TOPSP semantic presentation

begin


theorem Th1: :: T_1TOPSP:1
for T being non empty TopSpace
for A being non empty a_partition of the carrier of T
for y being Subset of (space A) holds (Proj A) " y = union y
proof
let T be non empty TopSpace; ::_thesis: for A being non empty a_partition of the carrier of T
for y being Subset of (space A) holds (Proj A) " y = union y
let A be non empty a_partition of the carrier of T; ::_thesis: for y being Subset of (space A) holds (Proj A) " y = union y
let y be Subset of (space A); ::_thesis: (Proj A) " y = union y
reconsider y = y as Subset of A by BORSUK_1:def_7;
(Proj A) " y = (proj A) " y by BORSUK_1:def_8
.= union y by EQREL_1:67 ;
hence  (Proj A) " y = union y ; ::_thesis: verum
end;

theorem Th2: :: T_1TOPSP:2
for T being non empty TopSpace
for S being non empty a_partition of the carrier of T
for A being Subset of (space S)
for B being Subset of T st B = union A holds
( A is closed iff B is closed )
proof
let T be non empty TopSpace; ::_thesis: for S being non empty a_partition of the carrier of T
for A being Subset of (space S)
for B being Subset of T st B = union A holds
( A is closed iff B is closed )
let S be non empty a_partition of the carrier of T; ::_thesis: for A being Subset of (space S)
for B being Subset of T st B = union A holds
( A is closed iff B is closed )
let A be Subset of (space S); ::_thesis: for B being Subset of T st B = union A holds
( A is closed iff B is closed )
let B be Subset of T; ::_thesis: ( B = union A implies ( A is closed iff B is closed ) )
reconsider C = A as Subset of S by BORSUK_1:def_7;
A1: ([#] T) \ (union A) = (union S) \ (union C) by EQREL_1:def_4
.= union (S \ A) by EQREL_1:43
.= union (([#] (space S)) \ A) by BORSUK_1:def_7 ;
assume A2: B = union A ; ::_thesis: ( A is closed iff B is closed )
thus  ( A is closed implies B is closed ) ::_thesis: ( B is closed implies A is closed )
proof
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def_7;
assume  A is closed ; ::_thesis: B is closed
then  ([#] (space S)) \ A is open by PRE_TOPC:def_3;
then  om in the topology of (space S) by PRE_TOPC:def_2;
then  ([#] T) \ B in the topology of T by A2, A1, BORSUK_1:27;
then  ([#] T) \ B is open by PRE_TOPC:def_2;
hence  B is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
thus  ( B is closed implies A is closed ) ::_thesis: verum
proof
reconsider om = ([#] (space S)) \ A as Subset of S by BORSUK_1:def_7;
assume  B is closed ; ::_thesis: A is closed
then  ([#] T) \ B is open by PRE_TOPC:def_3;
then  ([#] T) \ (union A) in the topology of T by A2, PRE_TOPC:def_2;
then  om in the topology of (space S) by A1, BORSUK_1:27;
then  ([#] (space S)) \ A is open by PRE_TOPC:def_2;
hence  A is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
end;

theorem Th3: :: T_1TOPSP:3
for T being non empty TopSpace holds  {  A where A is a_partition of the carrier of T : A is closed  }  is Part-Family of the carrier of T
proof
let T be non empty TopSpace; ::_thesis:  {  A where A is a_partition of the carrier of T : A is closed  }  is Part-Family of the carrier of T
set S =  {  A where A is a_partition of the carrier of T : A is closed  }  ;
A1: now__::_thesis:_for_B_being_set_st_B_in__{__A_where_A_is_a_partition_of_the_carrier_of_T_:_A_is_closed__}__holds_
B_is_a_partition_of_the_carrier_of_T
let B be set ; ::_thesis: ( B in  {  A where A is a_partition of the carrier of T : A is closed  }  implies B is a_partition of the carrier of T )
assume  B in  {  A where A is a_partition of the carrier of T : A is closed  }  ; ::_thesis: B is a_partition of the carrier of T
then  ex A being a_partition of the carrier of T st
( B = A & A is closed ) ;
hence  B is a_partition of the carrier of T ; ::_thesis: verum
end;
  {  A where A is a_partition of the carrier of T : A is closed  }  c= bool (bool the carrier of T)
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in  {  A where A is a_partition of the carrier of T : A is closed  }  or B in bool (bool the carrier of T) )
assume  B in  {  A where A is a_partition of the carrier of T : A is closed  }  ; ::_thesis: B in bool (bool the carrier of T)
then  ex A being a_partition of the carrier of T st
( B = A & A is closed ) ;
hence  B in bool (bool the carrier of T) ; ::_thesis: verum
end;
hence   {  A where A is a_partition of the carrier of T : A is closed  }  is Part-Family of the carrier of T by A1, EQREL_1:def_7; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
func Closed_Partitions T ->  non empty Part-Family of the carrier of T equals :: T_1TOPSP:def 1
 {  A where A is a_partition of the carrier of T : A is closed  }  ;
coherence
  {  A where A is a_partition of the carrier of T : A is closed  }  is non empty Part-Family of the carrier of T
proof
reconsider ct = { the carrier of T} as a_partition of the carrier of T by EQREL_1:39;
set F =  {  A where A is a_partition of the carrier of T : A is closed  }  ;
 for A being Subset of T st A in ct holds
A is closed
proof
let A be Subset of T; ::_thesis: ( A in ct implies A is closed )
assume  A in ct ; ::_thesis: A is closed
then  A = [#] T by TARSKI:def_1;
hence  A is closed ; ::_thesis: verum
end;
then  ct is closed by TOPS_2:def_2;
then  ct in  {  A where A is a_partition of the carrier of T : A is closed  }  ;
hence   {  A where A is a_partition of the carrier of T : A is closed  }  is non empty Part-Family of the carrier of T by Th3; ::_thesis: verum
end;
end;

:: deftheorem  defines Closed_Partitions T_1TOPSP:def_1_:_
 for T being non empty TopSpace holds Closed_Partitions T =  {  A where A is a_partition of the carrier of T : A is closed  }  ;

definition
let T be non empty TopSpace;
func T_1-reflex T ->  TopSpace equals :: T_1TOPSP:def 2
 space (Intersection (Closed_Partitions T));
correctness
coherence
space (Intersection (Closed_Partitions T)) is TopSpace;
;
end;

:: deftheorem  defines T_1-reflex T_1TOPSP:def_2_:_
 for T being non empty TopSpace holds T_1-reflex T = space (Intersection (Closed_Partitions T));

registration
let T be non empty TopSpace;
cluster T_1-reflex T ->  non empty strict ;
coherence
 ( T_1-reflex T is strict & not T_1-reflex T is empty ) ;
end;

theorem Th4: :: T_1TOPSP:4
for T being non empty TopSpace holds T_1-reflex T is T_1
proof
let T be non empty TopSpace; ::_thesis: T_1-reflex T is T_1
now__::_thesis:_for_p_being_Point_of_(T_1-reflex_T)_holds_{p}_is_closed
let p be Point of (T_1-reflex T); ::_thesis: {p} is closed
reconsider I = (Intersection (Closed_Partitions T)) \ {p} as Subset of (Intersection (Closed_Partitions T)) by XBOOLE_1:36;
A1: the carrier of (T_1-reflex T) = Intersection (Closed_Partitions T) by BORSUK_1:def_7;
then consider x being Element of T such that
A2: p = EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:42;
reconsider q = p as Subset of T by A2;
A3:  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  c= bool the carrier of T
proof
let Z be set ; :: according to TARSKI:def_3 ::_thesis: ( not Z in  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  or Z in bool the carrier of T )
assume  Z in  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  ; ::_thesis: Z in bool the carrier of T
then  ex Y being a_partition of the carrier of T st
( Z = EqClass (x,Y) & Y in Closed_Partitions T ) ;
hence  Z in bool the carrier of T ; ::_thesis: verum
end;
 not  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  is empty
proof
consider Y being set  such that
A4: Y in Closed_Partitions T by XBOOLE_0:def_1;
reconsider Y = Y as a_partition of the carrier of T by A4, EQREL_1:def_7;
 EqClass (x,Y) in  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  by A4;
hence  not  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  is empty ; ::_thesis: verum
end;
then reconsider m =  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  as non empty Subset-Family of T by A3;
reconsider m = m as non empty Subset-Family of T ;
A5: for A being Subset of T st A in m holds
A is closed
proof
let A be Subset of T; ::_thesis: ( A in m implies A is closed )
assume  A in m ; ::_thesis: A is closed
then consider S being a_partition of the carrier of T such that
A6: ( A = EqClass (x,S) & S in Closed_Partitions T ) ;
 ( ex B being a_partition of the carrier of T st
( S = B & B is closed ) & A in S ) by A6, EQREL_1:def_6;
hence  A is closed by TOPS_2:def_2; ::_thesis: verum
end;
 p = meet  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  by A2, EQREL_1:def_8;
then  q is closed by A5, PRE_TOPC:14;
then  ([#] T) \ q is open by PRE_TOPC:def_3;
then A7: ([#] T) \ p in the topology of T by PRE_TOPC:def_2;
 p in Intersection (Closed_Partitions T) by A1;
then  union ((Intersection (Closed_Partitions T)) \ {p}) in the topology of T by A7, EQREL_1:44;
then A8: I in  {  A where A is Subset of (Intersection (Closed_Partitions T)) : union A in the topology of T  }  ;
reconsider I = I as Subset of (space (Intersection (Closed_Partitions T))) by BORSUK_1:def_7;
reconsider I = I as Subset of (T_1-reflex T) ;
 ( the topology of (space (Intersection (Closed_Partitions T))) =  {  A where A is Subset of (Intersection (Closed_Partitions T)) : union A in the topology of T  }  & I = ([#] (T_1-reflex T)) \ {p} ) by BORSUK_1:def_7;
then  ([#] (T_1-reflex T)) \ {p} is open by A8, PRE_TOPC:def_2;
hence  {p} is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
hence  T_1-reflex T is T_1 by URYSOHN1:19; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster T_1-reflex T ->  T_1 ;
coherence
 T_1-reflex T is T_1 by Th4;
end;

registration
cluster non empty TopSpace-like T_1 for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is T_1 & not b1 is empty )
proof
set T = the non empty TopSpace;
take  T_1-reflex the non empty TopSpace ; ::_thesis: ( T_1-reflex the non empty TopSpace is T_1 & not T_1-reflex the non empty TopSpace is empty )
thus  ( T_1-reflex the non empty TopSpace is T_1 & not T_1-reflex the non empty TopSpace is empty ) ; ::_thesis: verum
end;
end;

definition
let T be non empty TopSpace;
func T_1-reflect T ->  continuous Function of T,(T_1-reflex T) equals :: T_1TOPSP:def 3
 Proj (Intersection (Closed_Partitions T));
correctness
coherence
Proj (Intersection (Closed_Partitions T)) is continuous Function of T,(T_1-reflex T);
;
end;

:: deftheorem  defines T_1-reflect T_1TOPSP:def_3_:_
 for T being non empty TopSpace holds T_1-reflect T = Proj (Intersection (Closed_Partitions T));

theorem Th5: :: T_1TOPSP:5
for T, T1 being non empty TopSpace
for f being continuous Function of T,T1 st T1 is T_1 holds
(  {  (f " {z}) where z is Element of T1 : z in rng f  }  is a_partition of the carrier of T & ( for A being Subset of T st A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  holds
A is closed ) )
proof
let T, T1 be non empty TopSpace; ::_thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
(  {  (f " {z}) where z is Element of T1 : z in rng f  }  is a_partition of the carrier of T & ( for A being Subset of T st A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  holds
A is closed ) )
let f be continuous Function of T,T1; ::_thesis: ( T1 is T_1 implies (  {  (f " {z}) where z is Element of T1 : z in rng f  }  is a_partition of the carrier of T & ( for A being Subset of T st A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  holds
A is closed ) ) )
assume A1: T1 is T_1 ; ::_thesis: (  {  (f " {z}) where z is Element of T1 : z in rng f  }  is a_partition of the carrier of T & ( for A being Subset of T st A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  holds
A is closed ) )
A2: dom f = the carrier of T by FUNCT_2:def_1;
thus   {  (f " {z}) where z is Element of T1 : z in rng f  }  is a_partition of the carrier of T ::_thesis: for A being Subset of T st A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  holds
A is closed
proof
  {  (f " {z}) where z is Element of T1 : z in rng f  }  c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (f " {z}) where z is Element of T1 : z in rng f  }  or y in bool the carrier of T )
assume  y in  {  (f " {z}) where z is Element of T1 : z in rng f  }  ; ::_thesis: y in bool the carrier of T
then  ex z being Element of T1 st
( y = f " {z} & z in rng f ) ;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
then reconsider fz =  {  (f " {z}) where z is Element of T1 : z in rng f  }  as Subset-Family of T ;
reconsider fz = fz as Subset-Family of T ;
A3: for A being Subset of T st A in fz holds
( A <> {} & ( for B being Subset of T holds
( not B in fz or A = B or A misses B ) ) )
proof
let A be Subset of T; ::_thesis: ( A in fz implies ( A <> {} & ( for B being Subset of T holds
( not B in fz or A = B or A misses B ) ) ) )
assume  A in fz ; ::_thesis: ( A <> {} & ( for B being Subset of T holds
( not B in fz or A = B or A misses B ) ) )
then consider z being Element of T1 such that
A4: A = f " {z} and
A5: z in rng f ;
consider y being set  such that
A6: ( y in dom f & z = f . y ) by A5, FUNCT_1:def_3;
 f . y in {(f . y)} by TARSKI:def_1;
hence  A <> {} by A4, A6, FUNCT_1:def_7; ::_thesis: for B being Subset of T holds
( not B in fz or A = B or A misses B )
let B be Subset of T; ::_thesis: ( not B in fz or A = B or A misses B )
assume  B in fz ; ::_thesis: ( A = B or A misses B )
then consider w being Element of T1 such that
A7: B = f " {w} and
 w in rng f ;
now__::_thesis:_(_not_A_misses_B_implies_A_=_B_)
assume  not A misses B ; ::_thesis: A = B
then consider v being set  such that
A8: v in A and
A9: v in B by XBOOLE_0:3;
 f . v in {z} by A4, A8, FUNCT_1:def_7;
then A10: f . v = z by TARSKI:def_1;
 f . v in {w} by A7, A9, FUNCT_1:def_7;
hence  A = B by A4, A7, A10, TARSKI:def_1; ::_thesis: verum
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
 the carrier of T c= union fz
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of T or y in union fz )
consider z being set  such that
A11: z = f . y ;
assume A12: y in the carrier of T ; ::_thesis: y in union fz
then A13: z in rng f by A2, A11, FUNCT_1:def_3;
then reconsider z = z as Element of T1 ;
A14: f " {z} in fz by A13;
 f . y in {(f . y)} by TARSKI:def_1;
then  y in f " {z} by A2, A12, A11, FUNCT_1:def_7;
hence  y in union fz by A14, TARSKI:def_4; ::_thesis: verum
end;
then  union fz = the carrier of T by XBOOLE_0:def_10;
hence   {  (f " {z}) where z is Element of T1 : z in rng f  }  is a_partition of the carrier of T by A3, EQREL_1:def_4; ::_thesis: verum
end;
thus  for A being Subset of T st A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  holds
A is closed ::_thesis: verum
proof
let A be Subset of T; ::_thesis: ( A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  implies A is closed )
assume  A in  {  (f " {z}) where z is Element of T1 : z in rng f  }  ; ::_thesis: A is closed
then consider z being Element of T1 such that
A15: A = f " {z} and
 z in rng f ;
 {z} is closed by A1, URYSOHN1:19;
hence  A is closed by A15, PRE_TOPC:def_6; ::_thesis: verum
end;
end;

theorem Th6: :: T_1TOPSP:6
for T, T1 being non empty TopSpace
for f being continuous Function of T,T1 st T1 is T_1 holds
for w being set
for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds
w c= f " {(f . x)}
proof
let T, T1 be non empty TopSpace; ::_thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
for w being set
for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds
w c= f " {(f . x)}
let f be continuous Function of T,T1; ::_thesis: ( T1 is T_1 implies for w being set
for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds
w c= f " {(f . x)} )
assume A1: T1 is T_1 ; ::_thesis: for w being set
for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds
w c= f " {(f . x)}
then reconsider fz =  {  (f " {z}) where z is Element of T1 : z in rng f  }  as a_partition of the carrier of T by Th5;
let w be set ; ::_thesis: for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds
w c= f " {(f . x)}
let x be Element of T; ::_thesis: ( w = EqClass (x,(Intersection (Closed_Partitions T))) implies w c= f " {(f . x)} )
 for A being Subset of T st A in fz holds
A is closed by A1, Th5;
then  fz is closed by TOPS_2:def_2;
then  fz in  {  B where B is a_partition of the carrier of T : B is closed  }  ;
then A2: EqClass (x,fz) in  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  ;
assume A3: w = EqClass (x,(Intersection (Closed_Partitions T))) ; ::_thesis: w c= f " {(f . x)}
A4: dom f = the carrier of T by FUNCT_2:def_1;
A5: f " {(f . x)} = EqClass (x,fz)
proof
reconsider fx = f . x as Element of T1 ;
 f . x in rng f by A4, FUNCT_1:def_3;
then A6: f " {fx} in fz ;
 f . x in {(f . x)} by TARSKI:def_1;
then  x in f " {(f . x)} by A4, FUNCT_1:def_7;
hence  f " {(f . x)} = EqClass (x,fz) by A6, EQREL_1:def_6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in w or y in f " {(f . x)} )
A7: EqClass (x,(Intersection (Closed_Partitions T))) = meet  {  (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T  }  by EQREL_1:def_8;
assume  y in w ; ::_thesis: y in f " {(f . x)}
hence  y in f " {(f . x)} by A3, A2, A5, A7, SETFAM_1:def_1; ::_thesis: verum
end;

theorem Th7: :: T_1TOPSP:7
for T, T1 being non empty TopSpace
for f being continuous Function of T,T1 st T1 is T_1 holds
for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} )
proof
let T, T1 be non empty TopSpace; ::_thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} )
let f be continuous Function of T,T1; ::_thesis: ( T1 is T_1 implies for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} ) )
assume A1: T1 is T_1 ; ::_thesis: for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} )
let w be set ; ::_thesis: ( w in the carrier of (T_1-reflex T) implies ex z being Element of T1 st
( z in rng f & w c= f " {z} ) )
assume  w in the carrier of (T_1-reflex T) ; ::_thesis: ex z being Element of T1 st
( z in rng f & w c= f " {z} )
then  w in Intersection (Closed_Partitions T) by BORSUK_1:def_7;
then consider x being Element of T such that
A2: w = EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:42;
reconsider x = x as Element of T ;
reconsider fx = f . x as Element of T1 ;
take  fx ; ::_thesis: ( fx in rng f & w c= f " {fx} )
 dom f = the carrier of T by FUNCT_2:def_1;
hence  ( fx in rng f & w c= f " {fx} ) by A1, A2, Th6, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th8: :: T_1TOPSP:8
for T, T1 being non empty TopSpace
for f being continuous Function of T,T1 st T1 is T_1 holds
ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T)
proof
let T, T1 be non empty TopSpace; ::_thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T)
let f be continuous Function of T,T1; ::_thesis: ( T1 is T_1 implies ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T) )
set g = T_1-reflect T;
A1: dom (T_1-reflect T) = the carrier of T by FUNCT_2:def_1;
defpred S1[ set , set ] means  for z being Element of T1 st z in rng f & $1 c= f " {z} holds
$2 = f " {z};
assume A2: T1 is T_1 ; ::_thesis: ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T)
then reconsider fx =  {  (f " {x}) where x is Element of T1 : x in rng f  }  as a_partition of the carrier of T by Th5;
A3: dom f = the carrier of T by FUNCT_2:def_1;
A4: for y being set st y in the carrier of (T_1-reflex T) holds
ex w being set st S1[y,w]
proof
let y be set ; ::_thesis: ( y in the carrier of (T_1-reflex T) implies ex w being set st S1[y,w] )
assume  y in the carrier of (T_1-reflex T) ; ::_thesis: ex w being set st S1[y,w]
then  y in Intersection (Closed_Partitions T) by BORSUK_1:def_7;
then consider x being Element of T such that
A5: y = EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:42;
reconsider x = x as Element of T ;
set w = f " {(f . x)};
take  f " {(f . x)} ; ::_thesis: S1[y,f " {(f . x)}]
let z be Element of T1; ::_thesis: ( z in rng f & y c= f " {z} implies f " {(f . x)} = f " {z} )
assume that
A6: z in rng f and
A7: y c= f " {z} ; ::_thesis: f " {(f . x)} = f " {z}
reconsider fix = f . x as Element of T1 ;
 f . x in rng f by A3, FUNCT_1:def_3;
then A8: f " {fix} in fx ;
 not y is empty by A5, EQREL_1:def_6;
then A9: ex z1 being set st z1 in y by XBOOLE_0:def_1;
 f " {z} in fx by A6;
then A10: ( f " {(f . x)} misses f " {z} or f " {(f . x)} = f " {z} ) by A8, EQREL_1:def_4;
 y c= f " {(f . x)} by A2, A5, Th6;
hence  f " {(f . x)} = f " {z} by A7, A10, A9, XBOOLE_0:3; ::_thesis: verum
end;
consider h1 being Function such that
A11: ( dom h1 = the carrier of (T_1-reflex T) & ( for y being set st y in the carrier of (T_1-reflex T) holds
S1[y,h1 . y] ) ) from CLASSES1:sch_1(A4);
defpred S2[ set , set ] means  for z being Element of T1 st z in rng f & $1 = f " {z} holds
$2 = z;
A12: for y being set st y in fx holds
ex w being set st S2[y,w]
proof
let y be set ; ::_thesis: ( y in fx implies ex w being set st S2[y,w] )
assume  y in fx ; ::_thesis: ex w being set st S2[y,w]
then consider w being Element of T1 such that
A13: y = f " {w} and
 w in rng f ;
take  w ; ::_thesis: S2[y,w]
let z be Element of T1; ::_thesis: ( z in rng f & y = f " {z} implies w = z )
assume that
A14: z in rng f and
A15: y = f " {z} ; ::_thesis: w = z
now__::_thesis:_not_z_<>_w
assume A16: z <> w ; ::_thesis: contradiction
consider v being set  such that
A17: v in dom f and
A18: z = f . v by A14, FUNCT_1:def_3;
 z in {z} by TARSKI:def_1;
then  v in f " {w} by A13, A15, A17, A18, FUNCT_1:def_7;
then  f . v in {w} by FUNCT_1:def_7;
hence  contradiction by A16, A18, TARSKI:def_1; ::_thesis: verum
end;
hence  w = z ; ::_thesis: verum
end;
consider h2 being Function such that
A19: ( dom h2 = fx & ( for y being set st y in fx holds
S2[y,h2 . y] ) ) from CLASSES1:sch_1(A12);
set h = h2 * h1;
A20: dom (h2 * h1) = the carrier of (T_1-reflex T)
proof
thus  dom (h2 * h1) c= the carrier of (T_1-reflex T) by A11, RELAT_1:25; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (T_1-reflex T) c= dom (h2 * h1)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of (T_1-reflex T) or z in dom (h2 * h1) )
assume A21: z in the carrier of (T_1-reflex T) ; ::_thesis: z in dom (h2 * h1)
then consider w being Element of T1 such that
A22: w in rng f and
A23: z c= f " {w} by A2, Th7;
 h1 . z = f " {w} by A11, A21, A22, A23;
then  h1 . z in dom h2 by A19, A22;
hence  z in dom (h2 * h1) by A11, A21, FUNCT_1:11; ::_thesis: verum
end;
A24: dom ((h2 * h1) * (T_1-reflect T)) = the carrier of T
proof
thus  dom ((h2 * h1) * (T_1-reflect T)) c= the carrier of T by A1, RELAT_1:25; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of T c= dom ((h2 * h1) * (T_1-reflect T))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of T or y in dom ((h2 * h1) * (T_1-reflect T)) )
assume A25: y in the carrier of T ; ::_thesis: y in dom ((h2 * h1) * (T_1-reflect T))
then  (T_1-reflect T) . y in rng (T_1-reflect T) by A1, FUNCT_1:def_3;
hence  y in dom ((h2 * h1) * (T_1-reflect T)) by A1, A20, A25, FUNCT_1:11; ::_thesis: verum
end;
A26: for x being set st x in dom f holds
f . x = ((h2 * h1) * (T_1-reflect T)) . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = ((h2 * h1) * (T_1-reflect T)) . x )
assume A27: x in dom f ; ::_thesis: f . x = ((h2 * h1) * (T_1-reflect T)) . x
then  (T_1-reflect T) . x in rng (T_1-reflect T) by A1, FUNCT_1:def_3;
then  (T_1-reflect T) . x in the carrier of (T_1-reflex T) ;
then  (T_1-reflect T) . x in Intersection (Closed_Partitions T) by BORSUK_1:def_7;
then consider y being Element of T such that
A28: (T_1-reflect T) . x = EqClass (y,(Intersection (Closed_Partitions T))) by EQREL_1:42;
reconsider x = x as Element of T by A27;
reconsider fix = f . x as Element of T1 ;
A29: x in EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:def_6;
 T_1-reflect T = proj (Intersection (Closed_Partitions T)) by BORSUK_1:def_8;
then  x in (T_1-reflect T) . x by EQREL_1:def_9;
then  EqClass (x,(Intersection (Closed_Partitions T))) meets EqClass (y,(Intersection (Closed_Partitions T))) by A28, A29, XBOOLE_0:3;
then A30: (T_1-reflect T) . x c= f " {fix} by A2, A28, Th6, EQREL_1:41;
A31: fix in rng f by A27, FUNCT_1:def_3;
then A32: f " {fix} in fx ;
((h2 * h1) * (T_1-reflect T)) . x = (h2 * h1) . ((T_1-reflect T) . x) by A24, FUNCT_1:12
.= h2 . (h1 . ((T_1-reflect T) . x)) by A11, FUNCT_1:13
.= h2 . (f " {fix}) by A11, A31, A30
.= f . x by A19, A31, A32 ;
hence  f . x = ((h2 * h1) * (T_1-reflect T)) . x ; ::_thesis: verum
end;
then A33: f = (h2 * h1) * (T_1-reflect T) by A3, A24, FUNCT_1:2;
A34: rng h2 c= the carrier of T1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h2 or y in the carrier of T1 )
assume  y in rng h2 ; ::_thesis: y in the carrier of T1
then consider w being set  such that
A35: w in dom h2 and
A36: y = h2 . w by FUNCT_1:def_3;
consider x being Element of T1 such that
A37: ( w = f " {x} & x in rng f ) by A19, A35;
 h2 . w = x by A19, A35, A37;
hence  y in the carrier of T1 by A36; ::_thesis: verum
end;
 rng (h2 * h1) c= rng h2
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (h2 * h1) or z in rng h2 )
thus  ( not z in rng (h2 * h1) or z in rng h2 ) by FUNCT_1:14; ::_thesis: verum
end;
then  rng (h2 * h1) c= the carrier of T1 by A34, XBOOLE_1:1;
then reconsider h = h2 * h1 as Function of the carrier of (T_1-reflex T), the carrier of T1 by A20, FUNCT_2:def_1, RELSET_1:4;
reconsider h = h as Function of (T_1-reflex T),T1 ;
 h is continuous
proof
let y be Subset of T1; :: according to PRE_TOPC:def_6 ::_thesis: ( not y is closed or h " y is closed )
reconsider hy = h " y as Subset of (space (Intersection (Closed_Partitions T))) ;
 union hy c= the carrier of T
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in union hy or z1 in the carrier of T )
assume  z1 in union hy ; ::_thesis: z1 in the carrier of T
then consider z2 being set  such that
A38: z1 in z2 and
A39: z2 in hy by TARSKI:def_4;
 z2 in the carrier of (space (Intersection (Closed_Partitions T))) by A39;
then  z2 in Intersection (Closed_Partitions T) by BORSUK_1:def_7;
hence  z1 in the carrier of T by A38; ::_thesis: verum
end;
then reconsider uhy = union hy as Subset of T ;
assume  y is closed ; ::_thesis: h " y is closed
then  (h * (T_1-reflect T)) " y is closed by A33, PRE_TOPC:def_6;
then  (T_1-reflect T) " (h " y) is closed by RELAT_1:146;
then  uhy is closed by Th1;
hence  h " y is closed by Th2; ::_thesis: verum
end;
then reconsider h = h as continuous Function of (T_1-reflex T),T1 ;
take  h ; ::_thesis: f = h * (T_1-reflect T)
thus  f = h * (T_1-reflect T) by A3, A24, A26, FUNCT_1:2; ::_thesis: verum
end;

definition
let T, S be non empty TopSpace;
let f be continuous Function of T,S;
func T_1-reflex f ->  continuous Function of (T_1-reflex T),(T_1-reflex S) means :: T_1TOPSP:def 4
(T_1-reflect S) * f = it * (T_1-reflect T);
existence
 ex b1 being continuous Function of (T_1-reflex T),(T_1-reflex S) st (T_1-reflect S) * f = b1 * (T_1-reflect T) by Th8;
uniqueness
 for b1, b2 being continuous Function of (T_1-reflex T),(T_1-reflex S) st (T_1-reflect S) * f = b1 * (T_1-reflect T) & (T_1-reflect S) * f = b2 * (T_1-reflect T) holds
b1 = b2
proof
let g1, g2 be continuous Function of (T_1-reflex T),(T_1-reflex S); ::_thesis: ( (T_1-reflect S) * f = g1 * (T_1-reflect T) & (T_1-reflect S) * f = g2 * (T_1-reflect T) implies g1 = g2 )
assume A1: ( (T_1-reflect S) * f = g1 * (T_1-reflect T) & (T_1-reflect S) * f = g2 * (T_1-reflect T) ) ; ::_thesis: g1 = g2
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_g1_holds_
g2_._x_=_g1_._x
let x be set ; ::_thesis: ( x in dom g1 implies g2 . x = g1 . x )
assume A3: x in dom g1 ; ::_thesis: g2 . x = g1 . x
then A4: x in the carrier of (T_1-reflex T) ;
A5: the carrier of (T_1-reflex T) = Intersection (Closed_Partitions T) by BORSUK_1:def_7;
then consider y being Element of T such that
A6: x = EqClass (y,(Intersection (Closed_Partitions T))) by A3, EQREL_1:42;
reconsider y = y as Element of T ;
set ty = (T_1-reflect T) . y;
 (T_1-reflect T) . y in Intersection (Closed_Partitions T) by A5;
then A7: ( (T_1-reflect T) . y misses x or (T_1-reflect T) . y = x ) by A4, A5, EQREL_1:def_4;
 T_1-reflect T = proj (Intersection (Closed_Partitions T)) by BORSUK_1:def_8;
then A8: ( dom (T_1-reflect T) = the carrier of T & y in (T_1-reflect T) . y ) by EQREL_1:def_9, FUNCT_2:def_1;
A9: y in x by A6, EQREL_1:def_6;
hence g2 . x = (g2 * (T_1-reflect T)) . y by A8, A7, FUNCT_1:13, XBOOLE_0:3
.= g1 . x by A1, A8, A9, A7, FUNCT_1:13, XBOOLE_0:3 ;
::_thesis: verum
end;
 ( dom g1 = the carrier of (T_1-reflex T) & dom g2 = the carrier of (T_1-reflex T) ) by FUNCT_2:def_1;
hence  g1 = g2 by A2, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines T_1-reflex T_1TOPSP:def_4_:_
 for T, S being non empty TopSpace
for f being continuous Function of T,S
for b4 being continuous Function of (T_1-reflex T),(T_1-reflex S) holds
( b4 = T_1-reflex f iff (T_1-reflect S) * f = b4 * (T_1-reflect T) );