let S, T be non empty TopSpace; ( 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
; T_0TOPSP:def 1 ( not S is arcwise_connected or T is arcwise_connected )
assume A2:
for a, b being Point of S holds a,b are_connected
; BORSUK_2:def 3 T is arcwise_connected
let a, b be Point of T; BORSUK_2:def 3 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; BORSUK_2:def 1 ( g is continuous & g . 0 = a & g . 1 = b )
h is continuous
by A1, TOPS_2:def 5;
hence
g is continuous
by A3; ( g . 0 = a & g . 1 = b )
A6:
( h is one-to-one & 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, TOPS_2:65
.=
a
by FUNCT_1:35
; 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, TOPS_2:65
.=
b
by FUNCT_1:35
; verum