let FT be non empty RelStr ; :: thesis: for x being Element of FT holds {x} is arcwise_connected

let x be Element of FT; :: thesis: {x} is arcwise_connected

set A = {x};

A1: rng <*x*> c= {x} by FINSEQ_1:39;

A2: <*x*> . 1 = x by FINSEQ_1:40;

then A3: <*x*> . (len <*x*>) = x by FINSEQ_1:40;

for x1, x2 being Element of FT st x1 in {x} & x2 in {x} holds

ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )

let x be Element of FT; :: thesis: {x} is arcwise_connected

set A = {x};

A1: rng <*x*> c= {x} by FINSEQ_1:39;

A2: <*x*> . 1 = x by FINSEQ_1:40;

then A3: <*x*> . (len <*x*>) = x by FINSEQ_1:40;

for x1, x2 being Element of FT st x1 in {x} & x2 in {x} holds

ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )

proof

hence
{x} is arcwise_connected
; :: thesis: verum
let x1, x2 be Element of FT; :: thesis: ( x1 in {x} & x2 in {x} implies ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) )

assume ( x1 in {x} & x2 in {x} ) ; :: thesis: ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )

then ( x1 = x & x2 = x ) by TARSKI:def 1;

hence ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) by A2, A3, A1; :: thesis: verum

end;( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) )

assume ( x1 in {x} & x2 in {x} ) ; :: thesis: ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )

then ( x1 = x & x2 = x ) by TARSKI:def 1;

hence ex f being FinSequence of FT st

( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) by A2, A3, A1; :: thesis: verum