let S, T be non empty TopSpace; ( 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
; T_0TOPSP:def 1 ( not S is pathwise_connected or T is pathwise_connected )
assume A2:
for a, b being Point of S holds a,b are_connected
; BORSUK_2:def 3 T is pathwise_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
;
take g = h * f; BORSUK_2:def 1 ( g is continuous & g . 0 = a & g . 1 = b )
h is continuous
by A1;
hence
g is continuous
by A3; ( 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
; 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
; verum