for a being Ordinal
for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a