:: deftheorem Def5 defines ScalarXCol MATRIX12:def 5 :
for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for l being Nat
for a being Element of K st l in Seg (width M) & n > 0 & m > 0 holds
for b₇ being Matrix of n,m,K holds
( b₇ = ScalarXCol (M,l,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,l)) ) & ( j <> l implies b₇ * (i,j) = M * (i,j) ) ) ) ) );