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