theorem Th47: :: ARYTM_3:47

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