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

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