theorem :: ORDINAL2:6

for A being Ordinal
for L being Sequence st dom L = succ A holds
last L = L . A by Th2;