theorem Th49: :: ORDINAL7:36
for A being finite Ordinal-Sequence
for b being Ordinal
for n being Nat holds b -exponent (A /^ n) = (b -exponent A) /^ n