theorem Th58: :: ORDINAL5:58

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