theorem :: COMPUT_1:90

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