:: deftheorem defines constant SEQM_3:def 10 :
for f being FinSequence holds
( f is constant iff for n, m being Nat st n in dom f & m in dom f holds
f . n = f . m );