:: deftheorem Def1 defines constant REVROT_1:def 1 :
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 );