theorem Th84: :: COMPUT_1:85

for i, j being Element of NAT holds [+] . <*i,j*> = i + j