theorem Th53: :: ORDINAL5:53

for a being Ordinal holds Sum^ <%a%> = a