theorem Th55: :: ORDINAL5:55

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