:: deftheorem Def11 defines Cantor-normal-form ORDINAL5:def 11 :
for A being Ordinal-Sequence holds
( A is Cantor-normal-form iff ( ( for a being Ordinal st a in dom A holds
A . a is Cantor-component ) & ( for a, b being Ordinal st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) ) );