theorem Th100: :: ORDINAL7:87

for a, b being Ordinal holds omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)