:: deftheorem defines continuous FINTOPO6:def 6 :
for FT being non empty RelStr
for f being FinSequence of FT holds
( f is continuous iff ( 1 <= len f & ( for i being Nat
for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds
f . (i + 1) in U_FT x1 ) ) );