theorem EQ2: :: ZMATRLIN:1

for D, E being non empty set
for M being Matrix of D
for L being Matrix of E
for i, j being Nat st M = L & [i,j] in Indices M holds
M * (i,j) = L * (i,j)