:: deftheorem Def6 defines RcolXScalar MATRIX12:def 6 :
for n, m being Nat
for K being non empty doubleLoopStr
for M being Matrix of n,m,K
for l, k being Nat
for a being Element of K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds
for b₈ being Matrix of n,m,K holds
( b₈ = RcolXScalar (M,l,k,a) iff ( len b₈ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies b₈ * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b₈ * (i,j) = M * (i,j) ) ) ) ) );