let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is pathwise_connected implies T is pathwise_connected )

given h being Function of S,T such that A1: h is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is pathwise_connected or T is pathwise_connected )

assume A2: for a, b being Point of S holds a,b are_connected ; :: according to BORSUK_2:def 3 :: thesis: T is pathwise_connected

let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

(h ") . a,(h ") . b are_connected by A2;

then consider f being Function of I[01],S such that

A3: f is continuous and

A4: f . 0 = (h ") . a and

A5: f . 1 = (h ") . b ;

take g = h * f; :: according to BORSUK_2:def 1 :: thesis: ( g is continuous & g . 0 = a & g . 1 = b )

h is continuous by A1;

hence g is continuous by A3; :: thesis: ( g . 0 = a & g . 1 = b )

A6: ( h is one-to-one & rng h = [#] T ) by A1;

thus g . 0 = h . ((h ") . a) by A4, BORSUK_1:def 14, FUNCT_2:15

.= (h * (h ")) . a by FUNCT_2:15

.= (id T) . a by A6, TOPS_2:52

.= a ; :: thesis: g . 1 = b

thus g . 1 = h . ((h ") . b) by A5, BORSUK_1:def 15, FUNCT_2:15

.= (h * (h ")) . b by FUNCT_2:15

.= (id T) . b by A6, TOPS_2:52

.= b ; :: thesis: verum

given h being Function of S,T such that A1: h is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is pathwise_connected or T is pathwise_connected )

assume A2: for a, b being Point of S holds a,b are_connected ; :: according to BORSUK_2:def 3 :: thesis: T is pathwise_connected

let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

(h ") . a,(h ") . b are_connected by A2;

then consider f being Function of I[01],S such that

A3: f is continuous and

A4: f . 0 = (h ") . a and

A5: f . 1 = (h ") . b ;

take g = h * f; :: according to BORSUK_2:def 1 :: thesis: ( g is continuous & g . 0 = a & g . 1 = b )

h is continuous by A1;

hence g is continuous by A3; :: thesis: ( g . 0 = a & g . 1 = b )

A6: ( h is one-to-one & rng h = [#] T ) by A1;

thus g . 0 = h . ((h ") . a) by A4, BORSUK_1:def 14, FUNCT_2:15

.= (h * (h ")) . a by FUNCT_2:15

.= (id T) . a by A6, TOPS_2:52

.= a ; :: thesis: g . 1 = b

thus g . 1 = h . ((h ") . b) by A5, BORSUK_1:def 15, FUNCT_2:15

.= (h * (h ")) . b by FUNCT_2:15

.= (id T) . b by A6, TOPS_2:52

.= b ; :: thesis: verum