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 5 ; :: 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 " = f " by A1, A2, 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