theorem :: NAT_1:47

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