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

proof

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

proof

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;

T_0-canonical_map S is open by Th8;
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;

A23: dom h = [#] (T_0-reflex S) by A1;
A24: for A being Subset of T st A is open holds
(f ") " A is open

proof

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

proof

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;

T_0-canonical_map T = h * ((T_0-canonical_map S) * f) by A6, RELAT_1:36;
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;

thus f is one-to-one by A5; :: thesis: ( f is continuous & f " is continuous )
[#] 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