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