theorem :: ORDINAL7:5

for a, b being Ordinal st 1 in a & a in b holds
a *^ b in exp (b,a)