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 S1[ set , set ] means $2 in f .: $1;
A1:
for C being set st C in the carrier of (T_0-reflex T) holds
ex y being set 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 set 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 set st C in the carrier of (T_0-reflex T) holds
h . C in f .: 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;
:: thesis: ( W is open implies h " W is open )
assume A7:
W is
open
;
:: thesis: h " W is open
set V =
h " W;
for
x being
set holds
(
x in union (h " W) iff
x in f " W )
proof
let x be
set ;
:: 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 " Wthen consider C being
set such that A8:
(
x in C &
C in h " W )
by TARSKI:def 4;
A9:
(
C in dom h &
h . C in W )
by A8, FUNCT_1:def 13;
consider p being
Point of
T such that A10:
C = Class (Indiscernibility T),
p
by A8, Th7;
A11:
(
[x,p] in Indiscernibility T &
x in the
carrier of
T )
by A8, A10, EQREL_1:27;
then
C = Class (Indiscernibility T),
x
by A10, EQREL_1:44;
then
(
f . x in W &
x in dom f )
by A5, A9, A11, FUNCT_2:def 1;
hence
x in f " W
by FUNCT_1:def 13;
:: thesis: verum
end;
assume
x in f " W
;
:: thesis: x in union (h " W)
then
(
f . x in W &
x is
Point of
T )
by FUNCT_1:def 13;
then
(
h . (Class (Indiscernibility T),x) in W &
x is
Point of
T &
Class (Indiscernibility T),
x is
Point of
(T_0-reflex T) )
by A5, Th7;
then
(
Class (Indiscernibility T),
x in h " W &
x in Class (Indiscernibility T),
x )
by EQREL_1:28, FUNCT_2:46;
hence
x in union (h " W)
by TARSKI:def 4;
:: thesis: verum
end;
then A12:
union (h " W) = f " W
by TARSKI:2;
f " W is
open
by A6, A7, TOPS_2:55;
then
union (h " W) in the
topology of
T
by A12, PRE_TOPC:def 5;
hence
h " W is
open
by Th6;
:: thesis: verum
end;
then reconsider h = h as continuous Function of (T_0-reflex T),T0 by A6, TOPS_2:55;
set H = h * (T_0-canonical_map T);
for x being set st x in the carrier of T holds
f . x = (h * (T_0-canonical_map T)) . x
proof
let x be
set ;
:: thesis: ( x in the carrier of T implies f . x = (h * (T_0-canonical_map T)) . x )
assume A13:
x in the
carrier of
T
;
:: thesis: f . x = (h * (T_0-canonical_map T)) . x
then A14:
x in dom (T_0-canonical_map T)
by FUNCT_2:def 1;
Class (Indiscernibility T),
x in Class (Indiscernibility T)
by A13, EQREL_1:def 5;
then A15:
Class (Indiscernibility T),
x in the
carrier of
(T_0-reflex T)
by BORSUK_1:def 10;
(T_0-canonical_map T) . x = Class (Indiscernibility T),
x
by A13, Th8;
then
(h * (T_0-canonical_map T)) . x = h . (Class (Indiscernibility T),x)
by A14, FUNCT_1:23;
then
(h * (T_0-canonical_map T)) . x in f .: (Class (Indiscernibility T),x)
by A4, A15;
then
(h * (T_0-canonical_map T)) . x in {(f . x)}
by A13, Th16;
hence
f . x = (h * (T_0-canonical_map T)) . x
by TARSKI:def 1;
:: thesis: verum
end;
then
f = h * (T_0-canonical_map T)
by FUNCT_2:18;
hence
ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)
; :: thesis: verum