theorem Th15: :: ORDINAL5:15

for a, b being Ordinal st b <> 0 & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi