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) & rng f = dom (h * (T_0-canonical_map S)) & f is one-to-one & T_0-canonical_map T = (h * (T_0-canonical_map S)) * f ) by A2, CLASSES1:85;
( dom f = the carrier of T & rng f = the carrier of S ) by A3, FUNCT_2:def 1;
then reconsider f = f as Function of T,S by FUNCT_2:def 1, RELSET_1:11;
take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
A4: ( [#] (T_0-reflex S) <> {} & [#] S <> {} & [#] T <> {} ) ;
thus A5: ( dom f = [#] T & rng f = [#] S ) by A3, FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A3; :: thesis: ( f is continuous & f " is continuous )
A6: ( dom h = [#] (T_0-reflex S) & rng h = [#] (T_0-reflex T) & h is one-to-one & h is continuous & h " is continuous ) by A1, TOPS_2:def 5;
for A being Subset of S st A is open holds
f " A is open

proof

let A be Subset of S; :: thesis: ( A is open implies f " A is open )
assume A7: A is open ; :: thesis: f " A is open
T_0-canonical_map S is open by Th12;
then A8: (T_0-canonical_map S) .: A is open by A7, Def2;
h " is continuous by A1, TOPS_2:def 5;
then A9: (h " ) " ((T_0-canonical_map S) .: A) is open by A4, A8, TOPS_2:55;
h .: ((T_0-canonical_map S) .: A) = (h " ) " ((T_0-canonical_map S) .: A) by A6, FUNCT_1:154;
then h .: ((T_0-canonical_map S) .: A) is open by A6, A9, TOPS_2:def 4;
then A10: (h * (T_0-canonical_map S)) .: A is open by RELAT_1:159;
set g = h * (T_0-canonical_map S);
set B = (h * (T_0-canonical_map S)) .: A;
[#] (T_0-reflex T) <> {} ;
then A11: (T_0-canonical_map T) " ((h * (T_0-canonical_map S)) .: A) is open by A10, TOPS_2:55;
A12: 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
A13: x1 in A and
A14: (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 A14, 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 A6, FUNCT_2:25;
hence x2 in A by A7, A13, Th10; :: thesis: verum

end;

(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 A3, RELAT_1:181;
hence f " A is open by A11, A12, Th2; :: thesis: verum

end;

hence f is continuous by A4, TOPS_2:55; :: thesis: f " is continuous
for A being Subset of T st A is open holds
(f " ) " A is open

proof

let A be Subset of T; :: thesis: ( A is open implies (f " ) " A is open )
assume A15: A is open ; :: thesis: (f " ) " A is open
set g = (h " ) * (T_0-canonical_map T);
A16: 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
A17: x1 in A and
A18: ((h " ) * (T_0-canonical_map T)) . x1 = ((h " ) * (T_0-canonical_map T)) . x2 ; :: thesis: x2 in A
A19: h " is one-to-one by A6, TOPS_2:63;
(h " ) . ((T_0-canonical_map T) . x1) = ((h " ) * (T_0-canonical_map T)) . x2 by A18, FUNCT_2:21;
then (h " ) . ((T_0-canonical_map T) . x1) = (h " ) . ((T_0-canonical_map T) . x2) by FUNCT_2:21;
then (T_0-canonical_map T) . x1 = (T_0-canonical_map T) . x2 by A19, FUNCT_2:25;
hence x2 in A by A15, A17, Th10; :: thesis: verum

end;

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

proof

T_0-canonical_map T is open by Th12;
then (T_0-canonical_map T) .: A is open by A15, Def2;
then A21: h " ((T_0-canonical_map T) .: A) is open by A6, 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 A6, TOPS_2:68;
hence (T_0-canonical_map S) " (((h " ) * (T_0-canonical_map T)) .: A) is open by A4, A21, TOPS_2:55; :: thesis: verum

end;

T_0-canonical_map T = h * ((T_0-canonical_map S) * f) by A3, 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 A6, 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 A3, A5, TOPS_2:65;
then T_0-canonical_map S = ((h " ) * (T_0-canonical_map T)) * (f " ) by FUNCT_2:23;
then (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;
hence (f " ) " A is open by A16, A20, Th2; :: thesis: verum

end;

hence f " is continuous by A4, TOPS_2:55; :: thesis: verum