:: deftheorem defines - MATRIX_1:def 9 :
for m, n being Nat
for K being non empty addLoopStr
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)) );