theorem Th84: :: COMPUT_1:85

for i, j being Nat holds [+] . <*i,j*> = i + j