theorem :: MATRIXR1:23

for D1, D2 being set
for A being Matrix of D1
for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)