theorem Th25: :: ORDINAL7:12

for a, b being Ordinal holds Sum^ <%a,b%> = a +^ b