theorem Th39: :: ORDINAL7:26

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