let a, b be Ordinal; :: thesis: Sum^ <%a,b%> = a +^ b
thus Sum^ <%a,b%> = Sum^ (<%a%> ^ <%b%>) by AFINSQ_1:def 5
.= (Sum^ <%a%>) +^ (Sum^ <%b%>) by Th24
.= (Sum^ <%a%>) +^ b by ORDINAL5:53
.= a +^ b by ORDINAL5:53 ; :: thesis: verum