theorem :: COMPUT_1:88

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