theorem :: ORDINAL7:45

for a, b being Ordinal st 1 in b holds
b -leading_coeff (exp (b,a)) = 1