for A being decreasing Ordinal-Sequence
for B being non-empty natural-valued Ordinal-Sequence st dom A = dom B holds
ex C being Cantor-normal-form Ordinal-Sequence st
( omega -exponent C = A & omega -leading_coeff C = B )