theorem :: ORDINAL7:43

for b being Ordinal holds b -leading_coeff 1 = 1