for a being Ordinal st 0 in a holds
ex n being Nat ex c being Ordinal st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in Segm n & c in exp (omega,(omega -exponent a)) )