let T, S be non empty TopSpace; :: thesis: ( ex h being Function of (),() st
( h is being_homeomorphism & T_0-canonical_map T,h * 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 (),() such that A1: h is being_homeomorphism and
A2: T_0-canonical_map T,h * are_fiberwise_equipotent ; :: thesis:
consider f being Function such that
A3: dom f = dom and
A4: rng f = dom (h * ) and
A5: f is one-to-one and
A6: T_0-canonical_map T = (h * ) * f by ;
A7: dom f = the carrier of T by ;
A8: h is continuous by A1;
A9: h is one-to-one by A1;
reconsider f = f as Function of T,S by ;
take f ; :: according to T_0TOPSP:def 1 :: thesis:
thus A10: ( dom f = [#] T & rng f = [#] S ) by ; :: according to TOPS_2:def 5 :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
A11: rng h = [#] () by A1;
A12: [#] () <> {} ;
A13: for A being Subset of S st A is open holds
f " A is open
proof
set g = h * ;
let A be Subset of S; :: thesis: ( A is open implies f " A is open )
set B = (h * ) .: 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 * ) . x1 = (h * ) . x2 holds
x2 in A
proof
let x1, x2 be Element of S; :: thesis: ( x1 in A & (h * ) . x1 = (h * ) . x2 implies x2 in A )
assume that
A17: x1 in A and
A18: (h * ) . x1 = (h * ) . x2 ; :: thesis: x2 in A
h . ( . x1) = (h * ) . x2 by ;
then h . ( . x1) = h . ( . x2) by FUNCT_2:15;
then (T_0-canonical_map S) . x1 = . x2 by ;
hence x2 in A by ; :: 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 ") " ( .: A) is open by ;
A20: h is onto by ;
h .: ( .: A) = (h ") " ( .: A) by ;
then h .: ( .: A) is open by ;
then A21: (h * ) .: A is open by RELAT_1:126;
[#] () <> {} ;
then A22: (T_0-canonical_map T) " ((h * ) .: A) is open by ;
(T_0-canonical_map T) " ((h * ) .: A) = f " ((h * ) " ((h * ) .: A)) by ;
hence f " A is open by ; :: thesis: verum
end;
A23: dom h = [#] () by A1;
A24: for A being Subset of T st A is open holds
(f ") " A is open
proof
set g = (h ") * ;
let A be Subset of T; :: thesis: ( A is open implies (f ") " A is open )
set B = ((h ") * ) .: A;
assume A25: A is open ; :: thesis: (f ") " A is open
A26: for x1, x2 being Element of T st x1 in A & ((h ") * ) . x1 = ((h ") * ) . x2 holds
x2 in A
proof
let x1, x2 be Element of T; :: thesis: ( x1 in A & ((h ") * ) . x1 = ((h ") * ) . x2 implies x2 in A )
assume that
A27: x1 in A and
A28: ((h ") * ) . x1 = ((h ") * ) . x2 ; :: thesis: x2 in A
(h ") . ( . x1) = ((h ") * ) . x2 by ;
then A29: (h ") . ( . x1) = (h ") . ( . x2) by FUNCT_2:15;
h " is one-to-one by ;
then (T_0-canonical_map T) . x1 = . x2 by ;
hence x2 in A by ; :: thesis: verum
end;
T_0-canonical_map T = h * ( * f) by ;
then (h ") * = ((h ") * h) * ( * f) by RELAT_1:36;
then (h ") * = (id the carrier of ()) * ( * f) by ;
then ((h ") * ) * (f ") = ( * f) * (f ") by FUNCT_2:17;
then ((h ") * ) * (f ") = * (f * (f ")) by RELAT_1:36;
then ((h ") * ) * (f ") = * (id the carrier of S) by ;
then T_0-canonical_map S = ((h ") * ) * (f ") by FUNCT_2:17;
then A30: (T_0-canonical_map S) " (((h ") * ) .: A) = (f ") " (((h ") * ) " (((h ") * ) .: 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 " ( .: A) is open by ;
((h ") * ) .: A = (h ") .: ( .: A) by RELAT_1:126;
then (T_0-canonical_map S) " (((h ") * ) .: A) = " (h " ( .: A)) by ;
then (T_0-canonical_map S) " (((h ") * ) .: A) is open by ;
hence (f ") " A is open by ; :: thesis: verum
end;
thus f is one-to-one by A5; :: thesis: ( f is continuous & f " is continuous )
[#] S <> {} ;
hence f is continuous by ; :: thesis: f " is continuous
[#] T <> {} ;
hence f " is continuous by ; :: thesis: verum