theorem :: ORDINAL1:33

for X being set
for L being Sequence of X
for A being Ordinal holds L | A is Sequence of X ;