let f be Ordinal-Sequence; :: thesis: ( f is empty implies f is Cantor-normal-form )
assume A1: f is empty ; :: thesis: f is Cantor-normal-form
hence for a being ordinal number st a in dom f holds
f . a is Cantor-component ; :: according to ORDINAL5:def 11 :: thesis: for a, b being ordinal number st a in b & b in dom f holds
omega -exponent (f . b) in omega -exponent (f . a)
thus for a, b being ordinal number st a in b & b in dom f holds
omega -exponent (f . b) in omega -exponent (f . a) by A1; :: thesis: verum