theorem Th4: :: MATRIX12:4

for l, n, m, i being Nat
for K being comRing
for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds
( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )