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