theorem :: VALUED_0:24

for X being non empty set
for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds
s is constant ;