let S, T be TopSpace; :: thesis: ( S,T are_homeomorphic & S is connected implies T is connected )
given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is connected or T is connected )
A2: rng f = [#] T by A1;
assume A3: S is connected ; :: thesis: T is connected
dom f = [#] S by A1;
then f .: ([#] S) = [#] T by A2, RELAT_1:113;
hence T is connected by A1, A3, CONNSP_1:14; :: thesis: verum