let S, T be non empty TopSpace; :: thesis: for f being Function of [:S,T:],[:T,S:] st f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> holds
f is being_homeomorphism
let f be Function of [:S,T:],[:T,S:]; :: thesis: ( f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> implies f is being_homeomorphism )
assume A1: f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> ; :: thesis: f is being_homeomorphism
thus dom f = [#] [:S,T:] by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] [:T,S:] & f is one-to-one & f is continuous & f " is continuous )
thus A2: rng f = [: the carrier of T, the carrier of S:] by A1, Th4
.= [#] [:T,S:] by BORSUK_1:def 2 ; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A1; :: thesis: ( f is continuous & f " is continuous )
thus f is continuous by A1, Th42; :: thesis: f " is continuous
f is onto by A2, FUNCT_2:def 3;
then f " = f " by A1, TOPS_2:def 4
.= <:(pr2 ( the carrier of T, the carrier of S)),(pr1 ( the carrier of T, the carrier of S)):> by A1, Th8 ;
hence f " is continuous by Th42; :: thesis: verum