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_{1}[ 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_{1}[C,y] )

for C being object st C in the carrier of (T_0-reflex T) holds

S_{1}[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_{1}[C,h . C]
;

A5: for p being Point of T holds h . (Class ((Indiscernibility T),p)) = f . p

A6: [#] T0 <> {} ;

for W being Subset of T0 st W is open holds

h " W is open

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

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

( 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

proof

ex h being Function of the carrier of (T_0-reflex T), the carrier of T0 st
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_{1}[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_{1}[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_{1}[C,y] )
by A3; :: thesis: verum

end;( y in the carrier of T0 & S

assume C in the carrier of (T_0-reflex T) ; :: thesis: ex y being object st

( y in the carrier of T0 & S

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

for C being object st C in the carrier of (T_0-reflex T) holds

S

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

A5: for p being Point of T holds h . (Class ((Indiscernibility T),p)) = f . p

proof

reconsider h = h as Function of (T_0-reflex T),T0 ;
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_{1}[ 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;Class ((Indiscernibility T),p) is Point of (T_0-reflex T) by Th3;

then S

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

A6: [#] T0 <> {} ;

for W being Subset of T0 st W is open holds

h " W is open

proof

then reconsider h = h as continuous Function of (T_0-reflex T),T0 by A6, TOPS_2:43;
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 )

then union (h " W) in the topology of T by A7;

hence h " W is open by Th2; :: thesis: verum

end;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

then
union (h " W) = f " W
by TARSKI:2;
let x be object ; :: thesis: ( x in union (h " W) iff x in f " 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;hereby :: thesis: ( x in f " W implies x in union (h " W) )

assume A13:
x in f " W
; :: thesis: 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;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

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

then union (h " W) in the topology of T by A7;

hence h " W is open by Th2; :: thesis: verum

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

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
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_{1}[ 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;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

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