let T, S be non empty TopSpace; :: thesis: ( ex h being Function of (T_0-reflex S),(T_0-reflex T) st

( h is being_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) implies T,S are_homeomorphic )

set F = T_0-canonical_map T;

set G = T_0-canonical_map S;

set TR = T_0-reflex T;

set SR = T_0-reflex S;

given h being Function of (T_0-reflex S),(T_0-reflex T) such that A1: h is being_homeomorphism and

A2: T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ; :: thesis: T,S are_homeomorphic

consider f being Function such that

A3: dom f = dom (T_0-canonical_map T) and

A4: rng f = dom (h * (T_0-canonical_map S)) and

A5: f is one-to-one and

A6: T_0-canonical_map T = (h * (T_0-canonical_map S)) * f by A2, CLASSES1:77;

A7: dom f = the carrier of T by A3, FUNCT_2:def 1;

A8: h is continuous by A1;

A9: h is one-to-one by A1;

reconsider f = f as Function of T,S by A4, A7, FUNCT_2:def 1, RELSET_1:4;

take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism

thus A10: ( dom f = [#] T & rng f = [#] S ) by A4, FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( f is one-to-one & f is continuous & f " is continuous )

A11: rng h = [#] (T_0-reflex T) by A1;

A12: [#] (T_0-reflex S) <> {} ;

A13: for A being Subset of S st A is open holds

f " A is open

A24: for A being Subset of T st A is open holds

(f ") " A is open

[#] S <> {} ;

hence f is continuous by A13, TOPS_2:43; :: thesis: f " is continuous

[#] T <> {} ;

hence f " is continuous by A24, TOPS_2:43; :: thesis: verum

( h is being_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) implies T,S are_homeomorphic )

set F = T_0-canonical_map T;

set G = T_0-canonical_map S;

set TR = T_0-reflex T;

set SR = T_0-reflex S;

given h being Function of (T_0-reflex S),(T_0-reflex T) such that A1: h is being_homeomorphism and

A2: T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ; :: thesis: T,S are_homeomorphic

consider f being Function such that

A3: dom f = dom (T_0-canonical_map T) and

A4: rng f = dom (h * (T_0-canonical_map S)) and

A5: f is one-to-one and

A6: T_0-canonical_map T = (h * (T_0-canonical_map S)) * f by A2, CLASSES1:77;

A7: dom f = the carrier of T by A3, FUNCT_2:def 1;

A8: h is continuous by A1;

A9: h is one-to-one by A1;

reconsider f = f as Function of T,S by A4, A7, FUNCT_2:def 1, RELSET_1:4;

take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism

thus A10: ( dom f = [#] T & rng f = [#] S ) by A4, FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( f is one-to-one & f is continuous & f " is continuous )

A11: rng h = [#] (T_0-reflex T) by A1;

A12: [#] (T_0-reflex S) <> {} ;

A13: for A being Subset of S st A is open holds

f " A is open

proof

A23:
dom h = [#] (T_0-reflex S)
by A1;
set g = h * (T_0-canonical_map S);

let A be Subset of S; :: thesis: ( A is open implies f " A is open )

set B = (h * (T_0-canonical_map S)) .: A;

A14: h " is continuous by A1;

assume A15: A is open ; :: thesis: f " A is open

A16: for x1, x2 being Element of S st x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 holds

x2 in A

then (T_0-canonical_map S) .: A is open by A15;

then A19: (h ") " ((T_0-canonical_map S) .: A) is open by A12, A14, TOPS_2:43;

A20: h is onto by A11, FUNCT_2:def 3;

h .: ((T_0-canonical_map S) .: A) = (h ") " ((T_0-canonical_map S) .: A) by A9, FUNCT_1:84;

then h .: ((T_0-canonical_map S) .: A) is open by A9, A19, A20, TOPS_2:def 4;

then A21: (h * (T_0-canonical_map S)) .: A is open by RELAT_1:126;

[#] (T_0-reflex T) <> {} ;

then A22: (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) is open by A21, TOPS_2:43;

(T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) = f " ((h * (T_0-canonical_map S)) " ((h * (T_0-canonical_map S)) .: A)) by A6, RELAT_1:146;

hence f " A is open by A22, A16, Th1; :: thesis: verum

end;let A be Subset of S; :: thesis: ( A is open implies f " A is open )

set B = (h * (T_0-canonical_map S)) .: A;

A14: h " is continuous by A1;

assume A15: A is open ; :: thesis: f " A is open

A16: for x1, x2 being Element of S st x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 holds

x2 in A

proof

T_0-canonical_map S is open
by Th8;
let x1, x2 be Element of S; :: thesis: ( x1 in A & (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 implies x2 in A )

assume that

A17: x1 in A and

A18: (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 ; :: thesis: x2 in A

h . ((T_0-canonical_map S) . x1) = (h * (T_0-canonical_map S)) . x2 by A18, FUNCT_2:15;

then h . ((T_0-canonical_map S) . x1) = h . ((T_0-canonical_map S) . x2) by FUNCT_2:15;

then (T_0-canonical_map S) . x1 = (T_0-canonical_map S) . x2 by A9, FUNCT_2:19;

hence x2 in A by A15, A17, Th6; :: thesis: verum

end;assume that

A17: x1 in A and

A18: (h * (T_0-canonical_map S)) . x1 = (h * (T_0-canonical_map S)) . x2 ; :: thesis: x2 in A

h . ((T_0-canonical_map S) . x1) = (h * (T_0-canonical_map S)) . x2 by A18, FUNCT_2:15;

then h . ((T_0-canonical_map S) . x1) = h . ((T_0-canonical_map S) . x2) by FUNCT_2:15;

then (T_0-canonical_map S) . x1 = (T_0-canonical_map S) . x2 by A9, FUNCT_2:19;

hence x2 in A by A15, A17, Th6; :: thesis: verum

then (T_0-canonical_map S) .: A is open by A15;

then A19: (h ") " ((T_0-canonical_map S) .: A) is open by A12, A14, TOPS_2:43;

A20: h is onto by A11, FUNCT_2:def 3;

h .: ((T_0-canonical_map S) .: A) = (h ") " ((T_0-canonical_map S) .: A) by A9, FUNCT_1:84;

then h .: ((T_0-canonical_map S) .: A) is open by A9, A19, A20, TOPS_2:def 4;

then A21: (h * (T_0-canonical_map S)) .: A is open by RELAT_1:126;

[#] (T_0-reflex T) <> {} ;

then A22: (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) is open by A21, TOPS_2:43;

(T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) = f " ((h * (T_0-canonical_map S)) " ((h * (T_0-canonical_map S)) .: A)) by A6, RELAT_1:146;

hence f " A is open by A22, A16, Th1; :: thesis: verum

A24: for A being Subset of T st A is open holds

(f ") " A is open

proof

thus
f is one-to-one
by A5; :: thesis: ( f is continuous & f " is continuous )
set g = (h ") * (T_0-canonical_map T);

let A be Subset of T; :: thesis: ( A is open implies (f ") " A is open )

set B = ((h ") * (T_0-canonical_map T)) .: A;

assume A25: A is open ; :: thesis: (f ") " A is open

A26: for x1, x2 being Element of T st x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 holds

x2 in A

then (h ") * (T_0-canonical_map T) = ((h ") * h) * ((T_0-canonical_map S) * f) by RELAT_1:36;

then (h ") * (T_0-canonical_map T) = (id the carrier of (T_0-reflex S)) * ((T_0-canonical_map S) * f) by A23, A11, A9, TOPS_2:52;

then ((h ") * (T_0-canonical_map T)) * (f ") = ((T_0-canonical_map S) * f) * (f ") by FUNCT_2:17;

then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (f * (f ")) by RELAT_1:36;

then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (id the carrier of S) by A5, A10, TOPS_2:52;

then T_0-canonical_map S = ((h ") * (T_0-canonical_map T)) * (f ") by FUNCT_2:17;

then A30: (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (f ") " (((h ") * (T_0-canonical_map T)) " (((h ") * (T_0-canonical_map T)) .: A)) by RELAT_1:146;

T_0-canonical_map T is open by Th8;

then (T_0-canonical_map T) .: A is open by A25;

then A31: h " ((T_0-canonical_map T) .: A) is open by A11, A8, TOPS_2:43;

((h ") * (T_0-canonical_map T)) .: A = (h ") .: ((T_0-canonical_map T) .: A) by RELAT_1:126;

then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (T_0-canonical_map S) " (h " ((T_0-canonical_map T) .: A)) by A11, A9, TOPS_2:55;

then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) is open by A12, A31, TOPS_2:43;

hence (f ") " A is open by A26, A30, Th1; :: thesis: verum

end;let A be Subset of T; :: thesis: ( A is open implies (f ") " A is open )

set B = ((h ") * (T_0-canonical_map T)) .: A;

assume A25: A is open ; :: thesis: (f ") " A is open

A26: for x1, x2 being Element of T st x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 holds

x2 in A

proof

T_0-canonical_map T = h * ((T_0-canonical_map S) * f)
by A6, RELAT_1:36;
let x1, x2 be Element of T; :: thesis: ( x1 in A & ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 implies x2 in A )

assume that

A27: x1 in A and

A28: ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 ; :: thesis: x2 in A

(h ") . ((T_0-canonical_map T) . x1) = ((h ") * (T_0-canonical_map T)) . x2 by A28, FUNCT_2:15;

then A29: (h ") . ((T_0-canonical_map T) . x1) = (h ") . ((T_0-canonical_map T) . x2) by FUNCT_2:15;

h " is one-to-one by A11, A9, TOPS_2:50;

then (T_0-canonical_map T) . x1 = (T_0-canonical_map T) . x2 by A29, FUNCT_2:19;

hence x2 in A by A25, A27, Th6; :: thesis: verum

end;assume that

A27: x1 in A and

A28: ((h ") * (T_0-canonical_map T)) . x1 = ((h ") * (T_0-canonical_map T)) . x2 ; :: thesis: x2 in A

(h ") . ((T_0-canonical_map T) . x1) = ((h ") * (T_0-canonical_map T)) . x2 by A28, FUNCT_2:15;

then A29: (h ") . ((T_0-canonical_map T) . x1) = (h ") . ((T_0-canonical_map T) . x2) by FUNCT_2:15;

h " is one-to-one by A11, A9, TOPS_2:50;

then (T_0-canonical_map T) . x1 = (T_0-canonical_map T) . x2 by A29, FUNCT_2:19;

hence x2 in A by A25, A27, Th6; :: thesis: verum

then (h ") * (T_0-canonical_map T) = ((h ") * h) * ((T_0-canonical_map S) * f) by RELAT_1:36;

then (h ") * (T_0-canonical_map T) = (id the carrier of (T_0-reflex S)) * ((T_0-canonical_map S) * f) by A23, A11, A9, TOPS_2:52;

then ((h ") * (T_0-canonical_map T)) * (f ") = ((T_0-canonical_map S) * f) * (f ") by FUNCT_2:17;

then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (f * (f ")) by RELAT_1:36;

then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (id the carrier of S) by A5, A10, TOPS_2:52;

then T_0-canonical_map S = ((h ") * (T_0-canonical_map T)) * (f ") by FUNCT_2:17;

then A30: (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (f ") " (((h ") * (T_0-canonical_map T)) " (((h ") * (T_0-canonical_map T)) .: A)) by RELAT_1:146;

T_0-canonical_map T is open by Th8;

then (T_0-canonical_map T) .: A is open by A25;

then A31: h " ((T_0-canonical_map T) .: A) is open by A11, A8, TOPS_2:43;

((h ") * (T_0-canonical_map T)) .: A = (h ") .: ((T_0-canonical_map T) .: A) by RELAT_1:126;

then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) = (T_0-canonical_map S) " (h " ((T_0-canonical_map T) .: A)) by A11, A9, TOPS_2:55;

then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) is open by A12, A31, TOPS_2:43;

hence (f ") " A is open by A26, A30, Th1; :: thesis: verum

[#] S <> {} ;

hence f is continuous by A13, TOPS_2:43; :: thesis: f " is continuous

[#] T <> {} ;

hence f " is continuous by A24, TOPS_2:43; :: thesis: verum