theorem Th85: :: COMPUT_1:86

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