for A being finite Ordinal-Sequence
for a being Ordinal holds Sum^ (A | a) c= Sum^ A