let T be non empty TopSpace; 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; 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; 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 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 (T_0-reflex T) holds
ex y being object st
( y in the carrier of T0 & S1[C,y] )
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
S1[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
S1[C,h . C]
;
A5:
for p being Point of T holds h . (Class ((Indiscernibility T),p)) = f . p
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;
( W is open implies h " W is open )
assume
W is
open
;
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 ;
( x in union (h " W) iff x in f " W )
hereby ( x in f " W implies x in union (h " W) )
assume
x in union (h " W)
;
x in f " Wthen 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;
verum
end;
assume A13:
x in f " W
;
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;
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;
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 ;
( x in the carrier of T implies f . x = (h * (T_0-canonical_map T)) . x )
assume A16:
x in the
carrier of
T
;
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;
S1[
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;
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; verum