for b being Ordinal
for n being Nat st 0 in Segm n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form