theorem Th9: :: ORDINAL5:9

for a, b being Ordinal st a is limit_ordinal & 0 in b holds
exp (a,b) is limit_ordinal