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 (),T0 st f = h *

let T0 be T_0-TopSpace; :: thesis: for f being continuous Function of T,T0 ex h being continuous Function of (),T0 st f = h *
let f be continuous Function of T,T0; :: thesis: ex h being continuous Function of (),T0 st f = h *
set F = T_0-canonical_map T;
set R = Indiscernibility T;
set TR = T_0-reflex T;
defpred S1[ 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 () holds
ex y being object st
( y in the carrier of T0 & S1[C,y] )
proof
let C be object ; :: thesis: ( C in the carrier of () implies ex y being object st
( y in the carrier of T0 & S1[C,y] ) )

assume C in the carrier of () ; :: thesis: ex y being object st
( y in the carrier of T0 & S1[C,y] )

then consider p being Point of T such that
A2: C = Class ((),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 ;
hence ex y being object st
( y in the carrier of T0 & S1[C,y] ) by A3; :: thesis: verum
end;
ex h being Function of the carrier of (), the carrier of T0 st
for C being object st C in the carrier of () holds
S1[C,h . C] from then consider h being Function of the carrier of (), the carrier of T0 such that
A4: for C being object st C in the carrier of () holds
S1[C,h . C] ;
A5: for p being Point of T holds h . (Class ((),p)) = f . p
proof
let p be Point of T; :: thesis: h . (Class ((),p)) = f . p
Class ((),p) is Point of () by Th3;
then S1[ Class ((),p),h . (Class ((),p))] by A4;
then h . (Class ((),p)) in f .: (Class ((),p)) ;
then h . (Class ((),p)) in {(f . p)} by Th12;
hence h . (Class ((),p)) = f . p by TARSKI:def 1; :: thesis: verum
end;
reconsider h = h as Function of (),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 ;
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 ((),p) by ;
x in the carrier of T by ;
then A11: x in dom f by FUNCT_2:def 1;
[x,p] in Indiscernibility T by ;
then A12: C = Class ((),x) by ;
h . C in W by ;
then f . x in W by A5, A8, A12;
hence x in f " W by ; :: 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 ((),x)) in W by ;
Class ((),x) is Point of () by ;
then A15: Class ((),x) in h " W by ;
x in Class ((),x) by ;
hence x in union (h " W) by ; :: 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 (),T0 by ;
set H = h * ;
for x being object st x in the carrier of T holds
f . x = (h * ) . x
proof
let x be object ; :: thesis: ( x in the carrier of T implies f . x = (h * ) . x )
assume A16: x in the carrier of T ; :: thesis: f . x = (h * ) . x
then Class ((),x) in Class () by EQREL_1:def 3;
then A17: Class ((),x) in the carrier of () by BORSUK_1:def 7;
( x in dom & . x = Class ((),x) ) by ;
then A18: (h * ) . x = h . (Class ((),x)) by FUNCT_1:13;
S1[ Class ((),x),h . (Class ((),x))] by ;
then (h * ) . x in f .: (Class ((),x)) by A18;
then (h * ) . x in {(f . x)} by ;
hence f . x = (h * ) . x by TARSKI:def 1; :: thesis: verum
end;
hence ex h being continuous Function of (),T0 st f = h * by FUNCT_2:12; :: thesis: verum