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