for i, j being ordinal Element of RAT+ holds i + j = i +^ j