theorem Th58: :: ORDINAL5:58

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