:: deftheorem defines constant VALUED_0:def 18 :
for X being non empty set
for s being sequence of X holds
( s is constant iff ex x being Element of X st
for n being Nat holds s . n = x );