let T be TopSpace; :: thesis: for S being non empty TopSpace
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
let S be non empty TopSpace; :: thesis: for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
let f be Function of T,S; :: thesis: ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )
hereby :: thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) implies f is being_homeomorphism )
assume A1: f is being_homeomorphism ; :: thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) )
hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) ; :: thesis: for P being Subset of T holds f .: (Cl P) = Cl (f .: P)
let P be Subset of T; :: thesis: f .: (Cl P) = Cl (f .: P)
f is continuous by A1;
then A3: f .: (Cl P) c= Cl (f .: P) by Th45;
f " is continuous by A1;
then A4: Cl ((f ") " P) c= (f ") " (Cl P) by Th44;
( (f ") " P = f .: P & (f ") " (Cl P) = f .: (Cl P) ) by A2, Th54;
hence f .: (Cl P) = Cl (f .: P) by A3, A4, XBOOLE_0:def 10; :: thesis: verum
end;
assume that
A5: dom f = [#] T and
A6: ( rng f = [#] S & f is one-to-one ) ; :: thesis: ( ex P being Subset of T st not f .: (Cl P) = Cl (f .: P) or f is being_homeomorphism )
assume A7: for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ; :: thesis: f is being_homeomorphism
thus ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A5, A6; :: according to TOPS_2:def 5 :: thesis: ( f is continuous & f " is continuous )
for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) by A7;
hence f is continuous by Th45; :: thesis: f " is continuous
now :: thesis: for P being Subset of T holds Cl ((f ") " P) c= (f ") " (Cl P)
let P be Subset of T; :: thesis: Cl ((f ") " P) c= (f ") " (Cl P)
( (f ") " P = f .: P & (f ") " (Cl P) = f .: (Cl P) ) by A6, Th54;
hence Cl ((f ") " P) c= (f ") " (Cl P) by A7; :: thesis: verum
end;
hence f " is continuous by Th44; :: thesis: verum