let c be Cantor-component Ordinal; :: thesis: c = (omega -leading_coeff c) *^ (exp (omega,(omega -exponent c)))
consider b being Ordinal, n being Nat such that
A1: ( 0 in Segm n & c = n *^ (exp (omega,b)) ) by ORDINAL5:def 9;
A2: omega -leading_coeff c = n by A1, Th57, ORDINAL1:def 12;
( 0 in n & n in omega ) by A1, ORDINAL1:def 12;
hence c = (omega -leading_coeff c) *^ (exp (omega,(omega -exponent c))) by A1, A2, ORDINAL5:58; :: thesis: verum