let T be non empty TopSpace; for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f is connected
let a, b be Point of T; for f being Path of a,b st a,b are_connected holds
rng f is connected
let f be Path of a,b; ( a,b are_connected implies rng f is connected )
assume A1:
a,b are_connected
; rng f is connected
A2:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
reconsider A = [.0,1.] as interval Subset of R^1 by TOPMETR:17;
reconsider B = A as Subset of I[01] by BORSUK_1:40;
A3:
B is connected
by CONNSP_1:23;
A4:
f is continuous
by A1, BORSUK_2:def 2;
f .: B = rng f
by A2, BORSUK_1:40, RELAT_1:113;
hence
rng f is connected
by A3, A4, TOPS_2:61; verum