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:
let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis:
(h ") . a,(h ") . b are_connected by A2;
then consider f being Function of I,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
.= (h * (h ")) . a by FUNCT_2:15
.= (id T) . a by
.= a ; :: thesis: g . 1 = b
thus g . 1 = h . ((h ") . b) by
.= (h * (h ")) . b by FUNCT_2:15
.= (id T) . b by
.= b ; :: thesis: verum