theorem Th46: :: ORDINAL7:33

for a, b being Ordinal holds b -exponent <%a%> = <%(b -exponent a)%>