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

let f be continuous Function of T,T1; :: thesis: ( T1 is T_1 implies ex h being continuous Function of (),T1 st f = h * () )
set g = T_1-reflect T;
A1: dom () = the carrier of T by FUNCT_2:def 1;
defpred S1[ object , object ] means ex D1 being set st
( D1 = \$1 & ( for z being Element of T1 st z in rng f & D1 c= f " {z} holds
\$2 = f " {z} ) );
assume A2: T1 is T_1 ; :: thesis: ex h being continuous Function of (),T1 st f = h * ()
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 object st y in the carrier of () holds
ex w being object st S1[y,w]
proof
let y be object ; :: thesis: ( y in the carrier of () implies ex w being object st S1[y,w] )
assume y in the carrier of () ; :: thesis: ex w being object st S1[y,w]
then y in Intersection by BORSUK_1:def 7;
then consider x being Element of T such that
A5: y = EqClass (x,) by EQREL_1:42;
reconsider x = x as Element of T ;
set w = f " {(f . x)};
reconsider yy = y as set by TARSKI:1;
take f " {(f . x)} ; :: thesis: S1[y,f " {(f . x)}]
take yy ; :: thesis: ( yy = y & ( for z being Element of T1 st z in rng f & yy c= f " {z} holds
f " {(f . x)} = f " {z} ) )

thus yy = y ; :: thesis: for z being Element of T1 st z in rng f & yy c= f " {z} holds
f " {(f . x)} = f " {z}

let z be Element of T1; :: thesis: ( z in rng f & yy c= f " {z} implies f " {(f . x)} = f " {z} )
assume that
A6: z in rng f and
A7: yy c= f " {z} ; :: thesis: f " {(f . x)} = f " {z}
reconsider fix = f . x as Element of T1 ;
f . x in rng f by ;
then A8: f " {fix} in fx ;
not yy is empty by ;
then A9: ex z1 being object st z1 in yy ;
f " {z} in fx by A6;
then A10: ( f " {(f . x)} misses f " {z} or f " {(f . x)} = f " {z} ) by ;
yy c= f " {(f . x)} by A2, A5, Th6;
hence f " {(f . x)} = f " {z} by ; :: thesis: verum
end;
consider h1 being Function such that
A11: ( dom h1 = the carrier of () & ( for y being object st y in the carrier of () holds
S1[y,h1 . y] ) ) from defpred S2[ object , object ] means for z being Element of T1 st z in rng f & \$1 = f " {z} holds
\$2 = z;
A12: for y being object st y in fx holds
ex w being object st S2[y,w]
proof
let y be object ; :: thesis: ( y in fx implies ex w being object st S2[y,w] )
assume y in fx ; :: thesis: ex w being object 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 object such that
A17: v in dom f and
A18: z = f . v by ;
z in {z} by TARSKI:def 1;
then v in f " {w} by ;
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 object st y in fx holds
S2[y,h2 . y] ) ) from set h = h2 * h1;
A20: dom (h2 * h1) = the carrier of ()
proof
thus dom (h2 * h1) c= the carrier of () by ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of () c= dom (h2 * h1)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of () or z in dom (h2 * h1) )
reconsider zz = z as set by TARSKI:1;
assume A21: z in the carrier of () ; :: thesis: z in dom (h2 * h1)
then consider w being Element of T1 such that
A22: w in rng f and
A23: zz c= f " {w} by ;
S1[z,h1 . z] by ;
then h1 . z = f " {w} by ;
then h1 . z in dom h2 by ;
hence z in dom (h2 * h1) by ; :: thesis: verum
end;
A24: dom ((h2 * h1) * ()) = the carrier of T
proof
thus dom ((h2 * h1) * ()) c= the carrier of T by ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= dom ((h2 * h1) * ())
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of T or y in dom ((h2 * h1) * ()) )
assume A25: y in the carrier of T ; :: thesis: y in dom ((h2 * h1) * ())
then (T_1-reflect T) . y in rng () by ;
hence y in dom ((h2 * h1) * ()) by ; :: thesis: verum
end;
A26: for x being object st x in dom f holds
f . x = ((h2 * h1) * ()) . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = ((h2 * h1) * ()) . x )
assume A27: x in dom f ; :: thesis: f . x = ((h2 * h1) * ()) . x
then (T_1-reflect T) . x in rng () by ;
then (T_1-reflect T) . x in the carrier of () ;
then (T_1-reflect T) . x in Intersection by BORSUK_1:def 7;
then consider y being Element of T such that
A28: (T_1-reflect T) . x = EqClass (y,) 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,) by EQREL_1:def 6;
T_1-reflect T = proj by BORSUK_1:def 8;
then x in () . x by EQREL_1:def 9;
then EqClass (x,) meets EqClass (y,) by ;
then A30: (T_1-reflect T) . x c= f " {fix} by ;
A31: fix in rng f by ;
then A32: f " {fix} in fx ;
A33: S1[(T_1-reflect T) . x,h1 . (() . x)] by A11;
((h2 * h1) * ()) . x = (h2 * h1) . (() . x) by
.= h2 . (h1 . (() . x)) by
.= h2 . (f " {fix}) by
.= f . x by ;
hence f . x = ((h2 * h1) * ()) . x ; :: thesis: verum
end;
then A34: f = (h2 * h1) * () by ;
A35: rng h2 c= the carrier of T1
proof
let y be object ; :: 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 object such that
A36: w in dom h2 and
A37: y = h2 . w by FUNCT_1:def 3;
consider x being Element of T1 such that
A38: ( w = f " {x} & x in rng f ) by ;
h2 . w = x by ;
hence y in the carrier of T1 by A37; :: thesis: verum
end;
rng (h2 * h1) c= rng h2 by FUNCT_1:14;
then rng (h2 * h1) c= the carrier of T1 by A35;
then reconsider h = h2 * h1 as Function of the carrier of (), the carrier of T1 by ;
reconsider h = h as Function of (),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 () ;
union hy c= the carrier of T
proof
let z1 be object ; :: 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
A39: z1 in z2 and
A40: z2 in hy by TARSKI:def 4;
z2 in the carrier of () by A40;
then z2 in Intersection by BORSUK_1:def 7;
hence z1 in the carrier of T by A39; :: thesis: verum
end;
then reconsider uhy = union hy as Subset of T ;
assume y is closed ; :: thesis: h " y is closed
then (h * ()) " y is closed by ;
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 (),T1 ;
take h ; :: thesis: f = h * ()
thus f = h * () by ; :: thesis: verum