for A being Ordinal-Sequence
for b, c being Ordinal holds b -exponent (A | c) = (b -exponent A) | c