:: deftheorem Def2 defines ScalarXLine MATRIX12:def 2 :
for n, m being Nat
for K being non empty multMagma
for M being Matrix of n,m,K
for l being Nat
for a being Element of K
for b₇ being Matrix of n,m,K holds
( b₇ = ScalarXLine (M,l,a) iff ( len b₇ = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies b₇ * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b₇ * (i,j) = M * (i,j) ) ) ) ) );