theorem Th64: :: ORDINAL7:51

for A being Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))