let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is arcwise_connected implies T is arcwise_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 arcwise_connected or T is arcwise_connected )
assume A2: for a, b being Point of S holds a,b are_connected ; :: according to BORSUK_2:def 3 :: thesis: T is arcwise_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 by BORSUK_2:def 1;
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, TOPS_2:def 5;
hence g is continuous by A3; :: thesis: ( g . 0 = a & g . 1 = b )
A6: h is one-to-one by A1, TOPS_2:def 5;
A7: rng h = [#] T by A1, TOPS_2:def 5;
thus g . 0 = h . ((h " ) . a) by A4, BORSUK_1:def 17, FUNCT_2:21
.= (h * (h " )) . a by FUNCT_2:21
.= (id T) . a by A6, A7, TOPS_2:65
.= a by FUNCT_1:35 ; :: thesis: g . 1 = b
thus g . 1 = h . ((h " ) . b) by A5, BORSUK_1:def 18, FUNCT_2:21
.= (h * (h " )) . b by FUNCT_2:21
.= (id T) . b by A6, A7, TOPS_2:65
.= b by FUNCT_1:35 ; :: thesis: verum