theorem :: VALUED_0:25

for X being non empty set
for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is V30()