let T be non empty TopSpace; :: thesis: for T0 being T_0-TopSpace
for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
let T0 be T_0-TopSpace; :: thesis: for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
let f be continuous Function of T,T0; :: thesis: ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
set F = T_0-canonical_map T;
set R = Indiscernibility T;
set TR = T_0-reflex T;
defpred S₁[ object , object ] means ex D1 being set st
( D1 = $1 & $2 in f .: D1 );
A1: for C being object st C in the carrier of (T_0-reflex T) holds
ex y being object st
( y in the carrier of T0 & S₁[C,y] )

proof

let C be object ; :: thesis: ( C in the carrier of (T_0-reflex T) implies ex y being object st
( y in the carrier of T0 & S₁[C,y] ) )
assume C in the carrier of (T_0-reflex T) ; :: thesis: ex y being object st
( y in the carrier of T0 & S₁[C,y] )
then consider p being Point of T such that
A2: C = Class ((Indiscernibility T),p) by Th3;
A3: f . p in {(f . p)} by TARSKI:def 1;
reconsider C = C as set by TARSKI:1;
f .: C = {(f . p)} by A2, Th12;
hence ex y being object st
( y in the carrier of T0 & S₁[C,y] ) by A3; :: thesis: verum

end;

ex h being Function of the carrier of (T_0-reflex T), the carrier of T0 st
for C being object st C in the carrier of (T_0-reflex T) holds
S₁[C,h . C] from FUNCT_2:sch 1(A1);
then consider h being Function of the carrier of (T_0-reflex T), the carrier of T0 such that
A4: for C being object st C in the carrier of (T_0-reflex T) holds
S₁[C,h . C] ;
A5: for p being Point of T holds h . (Class ((Indiscernibility T),p)) = f . p

proof

let p be Point of T; :: thesis: h . (Class ((Indiscernibility T),p)) = f . p
Class ((Indiscernibility T),p) is Point of (T_0-reflex T) by Th3;
then S₁[ Class ((Indiscernibility T),p),h . (Class ((Indiscernibility T),p))] by A4;
then h . (Class ((Indiscernibility T),p)) in f .: (Class ((Indiscernibility T),p)) ;
then h . (Class ((Indiscernibility T),p)) in {(f . p)} by Th12;
hence h . (Class ((Indiscernibility T),p)) = f . p by TARSKI:def 1; :: thesis: verum

end;

reconsider h = h as Function of (T_0-reflex T),T0 ;
A6: [#] T0 <> {} ;
for W being Subset of T0 st W is open holds
h " W is open

proof

let W be Subset of T0; :: thesis: ( W is open implies h " W is open )
assume W is open ; :: thesis: h " W is open
then A7: f " W is open by A6, TOPS_2:43;
set V = h " W;
for x being object holds
( x in union (h " W) iff x in f " W )

proof

let x be object ; :: thesis: ( x in union (h " W) iff x in f " W )

hereby :: thesis: ( x in f " W implies x in union (h " W) )

assume x in union (h " W) ; :: thesis: x in f " W
then consider C being set such that
A8: x in C and
A9: C in h " W by TARSKI:def 4;
consider p being Point of T such that
A10: C = Class ((Indiscernibility T),p) by A9, Th3;
x in the carrier of T by A8, A10;
then A11: x in dom f by FUNCT_2:def 1;
[x,p] in Indiscernibility T by A8, A10, EQREL_1:19;
then A12: C = Class ((Indiscernibility T),x) by A8, A10, EQREL_1:35;
h . C in W by A9, FUNCT_1:def 7;
then f . x in W by A5, A8, A12;
hence x in f " W by A11, FUNCT_1:def 7; :: thesis: verum

end;

assume A13: x in f " W ; :: thesis: x in union (h " W)
then f . x in W by FUNCT_1:def 7;
then A14: h . (Class ((Indiscernibility T),x)) in W by A5, A13;
Class ((Indiscernibility T),x) is Point of (T_0-reflex T) by A13, Th3;
then A15: Class ((Indiscernibility T),x) in h " W by A14, FUNCT_2:38;
x in Class ((Indiscernibility T),x) by A13, EQREL_1:20;
hence x in union (h " W) by A15, TARSKI:def 4; :: thesis: verum

end;

then union (h " W) = f " W by TARSKI:2;
then union (h " W) in the topology of T by A7;
hence h " W is open by Th2; :: thesis: verum

end;

then reconsider h = h as continuous Function of (T_0-reflex T),T0 by A6, TOPS_2:43;
set H = h * (T_0-canonical_map T);
for x being object st x in the carrier of T holds
f . x = (h * (T_0-canonical_map T)) . x

proof

let x be object ; :: thesis: ( x in the carrier of T implies f . x = (h * (T_0-canonical_map T)) . x )
assume A16: x in the carrier of T ; :: thesis: f . x = (h * (T_0-canonical_map T)) . x
then Class ((Indiscernibility T),x) in Class (Indiscernibility T) by EQREL_1:def 3;
then A17: Class ((Indiscernibility T),x) in the carrier of (T_0-reflex T) by BORSUK_1:def 7;
( x in dom (T_0-canonical_map T) & (T_0-canonical_map T) . x = Class ((Indiscernibility T),x) ) by A16, Th4, FUNCT_2:def 1;
then A18: (h * (T_0-canonical_map T)) . x = h . (Class ((Indiscernibility T),x)) by FUNCT_1:13;
S₁[ Class ((Indiscernibility T),x),h . (Class ((Indiscernibility T),x))] by A4, A17;
then (h * (T_0-canonical_map T)) . x in f .: (Class ((Indiscernibility T),x)) by A18;
then (h * (T_0-canonical_map T)) . x in {(f . x)} by A16, Th12;
hence f . x = (h * (T_0-canonical_map T)) . x by TARSKI:def 1; :: thesis: verum

end;

hence ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T) by FUNCT_2:12; :: thesis: verum