theorem Th47: :: ORDINAL7:34

for A, B being Ordinal-Sequence
for b being Ordinal holds b -exponent (A ^ B) = (b -exponent A) ^ (b -exponent B)