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:85;
A7: dom f = the carrier of T by A3, FUNCT_2:def 1;
A8: h is continuous by A1, TOPS_2:def 5;
A9: h is one-to-one by A1, TOPS_2:def 5;
reconsider f = f as Function of T,S by A4, A7, FUNCT_2:def 1, RELSET_1:11;
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, TOPS_2:def 5;
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, TOPS_2:def 5;
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:21;
then h . ((T_0-canonical_map S) . x1) = h . ((T_0-canonical_map S) . x2) by FUNCT_2:21;
then (T_0-canonical_map S) . x1 = (T_0-canonical_map S) . x2 by A9, FUNCT_2:25;
hence x2 in A by A15, A17, Th10; :: thesis: verum

end;

T_0-canonical_map S is open by Th12;
then (T_0-canonical_map S) .: A is open by A15, Def2;
then A19: (h ") " ((T_0-canonical_map S) .: A) is open by A12, A14, TOPS_2:55;
h .: ((T_0-canonical_map S) .: A) = (h ") " ((T_0-canonical_map S) .: A) by A9, FUNCT_1:154;
then h .: ((T_0-canonical_map S) .: A) is open by A11, A9, A19, TOPS_2:def 4;
then A20: (h * (T_0-canonical_map S)) .: A is open by RELAT_1:159;
[#] (T_0-reflex T) <> {} ;
then A21: (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) is open by A20, TOPS_2:55;
(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:181;
hence f " A is open by A21, A16, Th2; :: thesis: verum

end;

A22: dom h = [#] (T_0-reflex S) by A1, TOPS_2:def 5;
A23: 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 A24: A is open ; :: thesis: (f ") " A is open
A25: 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
A26: x1 in A and
A27: ((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 A27, FUNCT_2:21;
then A28: (h ") . ((T_0-canonical_map T) . x1) = (h ") . ((T_0-canonical_map T) . x2) by FUNCT_2:21;
h " is one-to-one by A11, A9, TOPS_2:63;
then (T_0-canonical_map T) . x1 = (T_0-canonical_map T) . x2 by A28, FUNCT_2:25;
hence x2 in A by A24, A26, Th10; :: thesis: verum

end;

T_0-canonical_map T = h * ((T_0-canonical_map S) * f) by A6, RELAT_1:55;
then (h ") * (T_0-canonical_map T) = ((h ") * h) * ((T_0-canonical_map S) * f) by RELAT_1:55;
then (h ") * (T_0-canonical_map T) = (id the carrier of (T_0-reflex S)) * ((T_0-canonical_map S) * f) by A22, A11, A9, TOPS_2:65;
then ((h ") * (T_0-canonical_map T)) * (f ") = ((T_0-canonical_map S) * f) * (f ") by FUNCT_2:23;
then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (f * (f ")) by RELAT_1:55;
then ((h ") * (T_0-canonical_map T)) * (f ") = (T_0-canonical_map S) * (id the carrier of S) by A5, A10, TOPS_2:65;
then T_0-canonical_map S = ((h ") * (T_0-canonical_map T)) * (f ") by FUNCT_2:23;
then A29: (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:181;
T_0-canonical_map T is open by Th12;
then (T_0-canonical_map T) .: A is open by A24, Def2;
then A30: h " ((T_0-canonical_map T) .: A) is open by A11, A8, TOPS_2:55;
((h ") * (T_0-canonical_map T)) .: A = (h ") .: ((T_0-canonical_map T) .: A) by RELAT_1:159;
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:68;
then (T_0-canonical_map S) " (((h ") * (T_0-canonical_map T)) .: A) is open by A12, A30, TOPS_2:55;
hence (f ") " A is open by A25, A29, Th2; :: 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:55; :: thesis: f " is continuous
[#] T <> {} ;
hence f " is continuous by A23, TOPS_2:55; :: thesis: verum