theorem :: ORDINAL5:7

for a, b being Ordinal
for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)