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) )
assume A1: 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 Th13;
set g = T_1-reflect T;
A2: ( dom f = the carrier of T & rng f c= the carrier of T1 ) by FUNCT_2:def 1;
A3: ( dom (T_1-reflect T) = the carrier of T & rng (T_1-reflect T) c= the carrier of (T_1-reflex 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};
A7: 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 10;
then consider x being Element of T such that
A8: y = EqClass x,(Intersection (Closed_Partitions T)) by EQREL_1:51;
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 A9: ( z in rng f & y c= f " {z} ) ; :: thesis: f " {(f . x)} = f " {z}
then A10: f " {z} in fx ;
A11: f . x in rng f by A2, FUNCT_1:def 5;
reconsider fix = f . x as Element of T1 ;
f " {fix} in fx by A11;
then A12: ( f " {(f . x)} misses f " {z} or f " {(f . x)} = f " {z} ) by A10, EQREL_1:def 6;
A13: ( y c= f " {(f . x)} & y c= f " {z} ) by A1, A8, A9, Th14;
not y is empty by A8, EQREL_1:def 8;
then consider z1 being set such that
A14: z1 in y by XBOOLE_0:def 1;
thus f " {(f . x)} = f " {z} by A12, A13, A14, XBOOLE_0:3; :: thesis: verum
end;
consider h1 being Function such that
A15: ( 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(A7);
 defpred S2[ set , set ] means for z being Element of T1 st z in rng f & $1 = f " {z} holds
$2 = z;
A19: 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
A20: ( y = f " {w} & 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 A21: ( z in rng f & y = f " {z} ) ; :: thesis: w = z
now
assume A22: z <> w ; :: thesis: contradiction
consider v being set such that
A23: ( v in dom f & z = f . v ) by A21, FUNCT_1:def 5;
z in {z} by TARSKI:def 1;
then v in f " {w} by A20, A21, A23, FUNCT_1:def 13;
then f . v in {w} by FUNCT_1:def 13;
hence contradiction by A22, A23, TARSKI:def 1; :: thesis: verum
end;
hence w = z ; :: thesis: verum
end;
consider h2 being Function such that
A24: ( dom h2 = fx & ( for y being set st y in fx holds
S2[y,h2 . y] ) ) from CLASSES1:sch 1(A19);
 set h = h2 * h1;
A25: dom (h2 * h1) = the carrier of (T_1-reflex T)
proof
thus dom (h2 * h1) c= the carrier of (T_1-reflex T) by A15, RELAT_1:44; :: 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 A26: z in the carrier of (T_1-reflex T) ; :: thesis: z in dom (h2 * h1)
then consider w being Element of T1 such that
A27: ( w in rng f & z c= f " {w} ) by A1, Th15;
h1 . z = f " {w} by A15, A26, A27;
then h1 . z in dom h2 by A24, A27;
hence z in dom (h2 * h1) by A15, A26, FUNCT_1:21; :: thesis: verum
end;
A28: 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:25; :: thesis: verum
end;
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
A29: ( w in dom h2 & y = h2 . w ) by FUNCT_1:def 5;
consider x being Element of T1 such that
A30: ( w = f " {x} & x in rng f ) by A24, A29;
h2 . w = x by A24, A29, A30;
hence y in the carrier of T1 by A29; :: thesis: verum
end;
then A31: rng (h2 * h1) c= the carrier of T1 by A28, XBOOLE_1:1;
A32: 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 A3, RELAT_1:44; :: 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 A33: 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 A3, FUNCT_1:def 5;
hence y in dom ((h2 * h1) * (T_1-reflect T)) by A3, A25, A33, FUNCT_1:21; :: thesis: verum
end;
A34: f = (h2 * h1) * (T_1-reflect T)
proof
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 A35: 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 A3, FUNCT_1:def 5;
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 10;
then consider y being Element of T such that
A36: (T_1-reflect T) . x = EqClass y,(Intersection (Closed_Partitions T)) by EQREL_1:51;
reconsider x = x as Element of T by A35;
T_1-reflect T = proj (Intersection (Closed_Partitions T)) by BORSUK_1:def 11;
then A37: x in (T_1-reflect T) . x by BORSUK_1:def 1;
x in EqClass x,(Intersection (Closed_Partitions T)) by EQREL_1:def 8;
then A38: EqClass x,(Intersection (Closed_Partitions T)) meets EqClass y,(Intersection (Closed_Partitions T)) by A36, A37, XBOOLE_0:3;
reconsider fix = f . x as Element of T1 ;
(T_1-reflect T) . x = EqClass x,(Intersection (Closed_Partitions T)) by A36, A38, EQREL_1:50;
then A39: ( fix in rng f & (T_1-reflect T) . x c= f " {fix} ) by A1, A35, Th14, FUNCT_1:def 5;
then A40: f " {fix} in fx ;
((h2 * h1) * (T_1-reflect T)) . x = (h2 * h1) . ((T_1-reflect T) . x) by A32, FUNCT_1:22
.= h2 . (h1 . ((T_1-reflect T) . x)) by A15, FUNCT_1:23
.= h2 . (f " {fix}) by A15, A39
.= f . x by A24, A39, A40 ;
hence f . x = ((h2 * h1) * (T_1-reflect T)) . x ; :: thesis: verum
end;
hence f = (h2 * h1) * (T_1-reflect T) by A2, A32, FUNCT_1:9; :: thesis: verum
end;
reconsider h = h2 * h1 as Function of the carrier of (T_1-reflex T),the carrier of T1 by A25, A31, FUNCT_2:def 1, RELSET_1:11;
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 12 :: thesis: ( not y is closed or h " y is closed )
assume A41: y is closed ; :: thesis: 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
A42: ( z1 in z2 & z2 in hy ) by TARSKI:def 4;
z2 in the carrier of (space (Intersection (Closed_Partitions T))) by A42;
then z2 in Intersection (Closed_Partitions T) by BORSUK_1:def 10;
hence z1 in the carrier of T by A42; :: thesis: verum
end;
then reconsider uhy = union hy as Subset of T ;
(h * (T_1-reflect T)) " y is closed by A34, A41, PRE_TOPC:def 12;
then (T_1-reflect T) " (h " y) is closed by RELAT_1:181;
then uhy is closed by Th2;
hence h " y is closed by Th5; :: 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 A34; :: thesis: verum