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

let f be continuous Function of T,T1; :: thesis: ( T1 is T_1 implies ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T) )

set g = T_1-reflect T;

A1: dom (T_1-reflect T) = the carrier of T by FUNCT_2:def 1;

defpred S_{1}[ 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 (T_1-reflex T),T1 st f = h * (T_1-reflect T)

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 (T_1-reflex T) holds

ex w being object st S_{1}[y,w]

A11: ( dom h1 = the carrier of (T_1-reflex T) & ( for y being object st y in the carrier of (T_1-reflex T) holds

S_{1}[y,h1 . y] ) )
from CLASSES1:sch 1(A4);

defpred S_{2}[ 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 S_{2}[y,w]

A19: ( dom h2 = fx & ( for y being object st y in fx holds

S_{2}[y,h2 . y] ) )
from CLASSES1:sch 1(A12);

set h = h2 * h1;

A20: dom (h2 * h1) = the carrier of (T_1-reflex T)

f . x = ((h2 * h1) * (T_1-reflect T)) . x

A35: rng h2 c= the carrier of T1

then rng (h2 * h1) c= the carrier of T1 by A35;

then reconsider h = h2 * h1 as Function of the carrier of (T_1-reflex T), the carrier of T1 by A20, FUNCT_2:def 1, RELSET_1:4;

reconsider h = h as Function of (T_1-reflex T),T1 ;

h is continuous

take h ; :: thesis: f = h * (T_1-reflect T)

thus f = h * (T_1-reflect T) by A3, A24, A26, FUNCT_1:2; :: thesis: verum

ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T)

let f be continuous Function of T,T1; :: thesis: ( T1 is T_1 implies ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T) )

set g = T_1-reflect T;

A1: dom (T_1-reflect T) = the carrier of T by FUNCT_2:def 1;

defpred S

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

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 (T_1-reflex T) holds

ex w being object st S

proof

consider h1 being Function such that
let y be object ; :: thesis: ( y in the carrier of (T_1-reflex T) implies ex w being object st S_{1}[y,w] )

assume y in the carrier of (T_1-reflex T) ; :: thesis: ex w being object st S_{1}[y,w]

then y in Intersection (Closed_Partitions T) by BORSUK_1:def 7;

then consider x being Element of T such that

A5: y = EqClass (x,(Intersection (Closed_Partitions T))) 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: S_{1}[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 A3, FUNCT_1:def 3;

then A8: f " {fix} in fx ;

not yy is empty by A5, EQREL_1:def 6;

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 A8, EQREL_1:def 4;

yy c= f " {(f . x)} by A2, A5, Th6;

hence f " {(f . x)} = f " {z} by A7, A10, A9, XBOOLE_0:3; :: thesis: verum

end;assume y in the carrier of (T_1-reflex T) ; :: thesis: ex w being object st S

then y in Intersection (Closed_Partitions T) by BORSUK_1:def 7;

then consider x being Element of T such that

A5: y = EqClass (x,(Intersection (Closed_Partitions T))) 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: S

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 A3, FUNCT_1:def 3;

then A8: f " {fix} in fx ;

not yy is empty by A5, EQREL_1:def 6;

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 A8, EQREL_1:def 4;

yy c= f " {(f . x)} by A2, A5, Th6;

hence f " {(f . x)} = f " {z} by A7, A10, A9, XBOOLE_0:3; :: thesis: verum

A11: ( dom h1 = the carrier of (T_1-reflex T) & ( for y being object st y in the carrier of (T_1-reflex T) holds

S

defpred S

$2 = z;

A12: for y being object st y in fx holds

ex w being object st S

proof

consider h2 being Function such that
let y be object ; :: thesis: ( y in fx implies ex w being object st S_{2}[y,w] )

assume y in fx ; :: thesis: ex w being object st S_{2}[y,w]

then consider w being Element of T1 such that

A13: y = f " {w} and

w in rng f ;

take w ; :: thesis: S_{2}[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

end;assume y in fx ; :: thesis: ex w being object st S

then consider w being Element of T1 such that

A13: y = f " {w} and

w in rng f ;

take w ; :: thesis: S

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

hence
w = z
; :: thesis: verumassume A16:
z <> w
; :: thesis: contradiction

consider v being object such that

A17: v in dom f and

A18: z = f . v by A14, FUNCT_1:def 3;

z in {z} by TARSKI:def 1;

then v in f " {w} by A13, A15, A17, A18, FUNCT_1:def 7;

then f . v in {w} by FUNCT_1:def 7;

hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum

end;consider v being object such that

A17: v in dom f and

A18: z = f . v by A14, FUNCT_1:def 3;

z in {z} by TARSKI:def 1;

then v in f " {w} by A13, A15, A17, A18, FUNCT_1:def 7;

then f . v in {w} by FUNCT_1:def 7;

hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum

A19: ( dom h2 = fx & ( for y being object st y in fx holds

S

set h = h2 * h1;

A20: dom (h2 * h1) = the carrier of (T_1-reflex T)

proof

A24:
dom ((h2 * h1) * (T_1-reflect T)) = the carrier of T
thus
dom (h2 * h1) c= the carrier of (T_1-reflex T)
by A11, RELAT_1:25; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (T_1-reflex T) c= dom (h2 * h1)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of (T_1-reflex T) or z in dom (h2 * h1) )

reconsider zz = z as set by TARSKI:1;

assume A21: z in the carrier of (T_1-reflex T) ; :: 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 A2, Th7;

S_{1}[z,h1 . z]
by A11, A21;

then h1 . z = f " {w} by A22, A23;

then h1 . z in dom h2 by A19, A22;

hence z in dom (h2 * h1) by A11, A21, FUNCT_1:11; :: thesis: verum

end;let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of (T_1-reflex T) or z in dom (h2 * h1) )

reconsider zz = z as set by TARSKI:1;

assume A21: z in the carrier of (T_1-reflex T) ; :: 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 A2, Th7;

S

then h1 . z = f " {w} by A22, A23;

then h1 . z in dom h2 by A19, A22;

hence z in dom (h2 * h1) by A11, A21, FUNCT_1:11; :: thesis: verum

proof

A26:
for x being object st x in dom f holds
thus
dom ((h2 * h1) * (T_1-reflect T)) c= the carrier of T
by A1, RELAT_1:25; :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= dom ((h2 * h1) * (T_1-reflect T))

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of T or y in dom ((h2 * h1) * (T_1-reflect T)) )

assume A25: y in the carrier of T ; :: thesis: y in dom ((h2 * h1) * (T_1-reflect T))

then (T_1-reflect T) . y in rng (T_1-reflect T) by A1, FUNCT_1:def 3;

hence y in dom ((h2 * h1) * (T_1-reflect T)) by A1, A20, A25, FUNCT_1:11; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of T or y in dom ((h2 * h1) * (T_1-reflect T)) )

assume A25: y in the carrier of T ; :: thesis: y in dom ((h2 * h1) * (T_1-reflect T))

then (T_1-reflect T) . y in rng (T_1-reflect T) by A1, FUNCT_1:def 3;

hence y in dom ((h2 * h1) * (T_1-reflect T)) by A1, A20, A25, FUNCT_1:11; :: thesis: verum

f . x = ((h2 * h1) * (T_1-reflect T)) . x

proof

then A34:
f = (h2 * h1) * (T_1-reflect T)
by A3, A24, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom f implies f . x = ((h2 * h1) * (T_1-reflect T)) . x )

assume A27: x in dom f ; :: thesis: f . x = ((h2 * h1) * (T_1-reflect T)) . x

then (T_1-reflect T) . x in rng (T_1-reflect T) by A1, FUNCT_1:def 3;

then (T_1-reflect T) . x in the carrier of (T_1-reflex T) ;

then (T_1-reflect T) . x in Intersection (Closed_Partitions T) by BORSUK_1:def 7;

then consider y being Element of T such that

A28: (T_1-reflect T) . x = EqClass (y,(Intersection (Closed_Partitions T))) 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,(Intersection (Closed_Partitions T))) by EQREL_1:def 6;

T_1-reflect T = proj (Intersection (Closed_Partitions T)) by BORSUK_1:def 8;

then x in (T_1-reflect T) . x by EQREL_1:def 9;

then EqClass (x,(Intersection (Closed_Partitions T))) meets EqClass (y,(Intersection (Closed_Partitions T))) by A28, A29, XBOOLE_0:3;

then A30: (T_1-reflect T) . x c= f " {fix} by A2, A28, Th6, EQREL_1:41;

A31: fix in rng f by A27, FUNCT_1:def 3;

then A32: f " {fix} in fx ;

A33: S_{1}[(T_1-reflect T) . x,h1 . ((T_1-reflect T) . x)]
by A11;

((h2 * h1) * (T_1-reflect T)) . x = (h2 * h1) . ((T_1-reflect T) . x) by A24, FUNCT_1:12

.= h2 . (h1 . ((T_1-reflect T) . x)) by A11, FUNCT_1:13

.= h2 . (f " {fix}) by A31, A30, A33

.= f . x by A19, A31, A32 ;

hence f . x = ((h2 * h1) * (T_1-reflect T)) . x ; :: thesis: verum

end;assume A27: x in dom f ; :: thesis: f . x = ((h2 * h1) * (T_1-reflect T)) . x

then (T_1-reflect T) . x in rng (T_1-reflect T) by A1, FUNCT_1:def 3;

then (T_1-reflect T) . x in the carrier of (T_1-reflex T) ;

then (T_1-reflect T) . x in Intersection (Closed_Partitions T) by BORSUK_1:def 7;

then consider y being Element of T such that

A28: (T_1-reflect T) . x = EqClass (y,(Intersection (Closed_Partitions T))) 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,(Intersection (Closed_Partitions T))) by EQREL_1:def 6;

T_1-reflect T = proj (Intersection (Closed_Partitions T)) by BORSUK_1:def 8;

then x in (T_1-reflect T) . x by EQREL_1:def 9;

then EqClass (x,(Intersection (Closed_Partitions T))) meets EqClass (y,(Intersection (Closed_Partitions T))) by A28, A29, XBOOLE_0:3;

then A30: (T_1-reflect T) . x c= f " {fix} by A2, A28, Th6, EQREL_1:41;

A31: fix in rng f by A27, FUNCT_1:def 3;

then A32: f " {fix} in fx ;

A33: S

((h2 * h1) * (T_1-reflect T)) . x = (h2 * h1) . ((T_1-reflect T) . x) by A24, FUNCT_1:12

.= h2 . (h1 . ((T_1-reflect T) . x)) by A11, FUNCT_1:13

.= h2 . (f " {fix}) by A31, A30, A33

.= f . x by A19, A31, A32 ;

hence f . x = ((h2 * h1) * (T_1-reflect T)) . x ; :: thesis: verum

A35: rng h2 c= the carrier of T1

proof

rng (h2 * h1) c= rng h2
by FUNCT_1:14;
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 A19, A36;

h2 . w = x by A19, A36, A38;

hence y in the carrier of T1 by A37; :: thesis: verum

end;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 A19, A36;

h2 . w = x by A19, A36, A38;

hence y in the carrier of T1 by A37; :: thesis: verum

then rng (h2 * h1) c= the carrier of T1 by A35;

then reconsider h = h2 * h1 as Function of the carrier of (T_1-reflex T), the carrier of T1 by A20, FUNCT_2:def 1, RELSET_1:4;

reconsider h = h as Function of (T_1-reflex T),T1 ;

h is continuous

proof

then reconsider h = h as continuous Function of (T_1-reflex T),T1 ;
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 (space (Intersection (Closed_Partitions T))) ;

union hy c= the carrier of T

assume y is closed ; :: thesis: h " y is closed

then (h * (T_1-reflect T)) " y is closed by A34, PRE_TOPC:def 6;

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;reconsider hy = h " y as Subset of (space (Intersection (Closed_Partitions T))) ;

union hy c= the carrier of T

proof

then reconsider uhy = union hy as Subset of T ;
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 (space (Intersection (Closed_Partitions T))) by A40;

then z2 in Intersection (Closed_Partitions T) by BORSUK_1:def 7;

hence z1 in the carrier of T by A39; :: thesis: verum

end;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 (space (Intersection (Closed_Partitions T))) by A40;

then z2 in Intersection (Closed_Partitions T) by BORSUK_1:def 7;

hence z1 in the carrier of T by A39; :: thesis: verum

assume y is closed ; :: thesis: h " y is closed

then (h * (T_1-reflect T)) " y is closed by A34, PRE_TOPC:def 6;

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

take h ; :: thesis: f = h * (T_1-reflect T)

thus f = h * (T_1-reflect T) by A3, A24, A26, FUNCT_1:2; :: thesis: verum