:: deftheorem Def5 defines + MATRIX_1:def 5 :
for K being non empty doubleLoopStr
for n being Nat
for A, B, b₅ being Matrix of 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)) );