for i, j, k being natural Ordinal st k <> {} holds
(i / k) + (j / k) = (i +^ j) / k