:: deftheorem Def5 defines + MATRIX_1:def 8 :
for m, n being Nat
for K being non empty addMagma
for A, B, b₆ being Matrix of m,n,K holds
( b₆ = A + B iff for i, j being Nat st [i,j] in Indices A holds
b₆ * (i,j) = (A * (i,j)) + (B * (i,j)) );