:: deftheorem Def1 defines constant FINSEQ_6:def 11 :
for D being non empty set
for f being FinSequence of D holds
( f is constant iff for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m );