for i, j being Nat
for M1, M2 being Matrix of COMPLEX st [i,j] in Indices M1 holds
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j))