:: deftheorem defines last ORDINAL2:def 1 :
for L being Sequence holds last L = L . (union (dom L));