:: deftheorem defines lim ORDINAL2:def 11 :
for A being Ordinal
for fi being Ordinal-Sequence holds lim (A,fi) = lim (fi | A);