let FT be non empty RelStr ; :: thesis: for x being Element of FT holds <*x*> is continuous
let x be Element of FT; :: thesis: <*x*> is continuous
thus 1 <= len <*x*> by FINSEQ_1:39; :: according to FINTOPO6:def 6 :: thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len <*x*> & x1 = <*x*> . i holds
<*x*> . (i + 1) in U_FT x1
thus for i being Nat
for x1 being Element of FT st 1 <= i & i < len <*x*> & x1 = <*x*> . i holds
<*x*> . (i + 1) in U_FT x1 by FINSEQ_1:39; :: thesis: verum