:: deftheorem Def3 defines + MATRIX_3:def 3 :
for K being Ring
for A, B, b₄ being Matrix of K holds
( b₄ = A + B iff ( len b₄ = len A & width b₄ = width A & ( for i, j being Nat st [i,j] in Indices A holds
b₄ * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) );