theorem :: MATRIX_0:46

for i, j, n, m being Nat
for D being non empty set
for a being Element of D st [i,j] in Indices ((n,m) --> a) holds
((n,m) --> a) * (i,j) = a