theorem Th54: :: ORDINAL5:54

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