let S, T, V be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & T,V are_homeomorphic implies S,V are_homeomorphic )
assume A1: ( S,T are_homeomorphic & T,V are_homeomorphic ) ; :: thesis: S,V are_homeomorphic
then consider f being Function of S,T such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
consider g being Function of T,V such that
A3: g is being_homeomorphism by A1, T_0TOPSP:def 1;
g * f is being_homeomorphism by A2, A3, TOPS_2:71;
hence S,V are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum