theorem Th22: :: ORDINAL7:9

for a, b, c being Ordinal st a c= c holds
b -exponent a c= b -exponent c