theorem :: ORDINAL7:25

for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st omega -exponent (last A) <> 0 holds
A ^ <%n%> is Cantor-normal-form