theorem :: ORDINAL7:37
for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
rng (omega -exponent A) misses rng (omega -exponent B)