for X being non empty set
for s being sequence of X holds s ^\ 0 = s