let i, j, k be natural Ordinal; :: thesis: ( k <> {} implies (i / k) + (j / k) = (i +^ j) / k )
assume A1: k <> {} ; :: thesis: (i / k) + (j / k) = (i +^ j) / k
hence (i / k) + (j / k) = ((i *^ k) +^ (j *^ k)) / (k *^ k) by Th46
.= ((i +^ j) *^ k) / (k *^ k) by ORDINAL3:46
.= (i +^ j) / k by A1, Th44 ;
:: thesis: verum