theorem Th57: :: ORDINAL7:44

for a, b, c being Ordinal st c in b holds
b -leading_coeff (c *^ (exp (b,a))) = c