for A, C being Ordinal
for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A)