theorem :: COMPUT_1:90

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