theorem Th65: :: ORDINAL7:52

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)))