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