for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi