consider b being Ordinal, n being Nat such that
A1: ( 0 in Segm n & c = n *^ (exp (omega,b)) ) by ORDINAL5:def 9;
thus ( omega -leading_coeff c is natural & not omega -leading_coeff c is empty ) by A1, Th57, ORDINAL1:def 12; :: thesis: verum