theorem Th34: :: MATRIX11:34

for l, n being Nat
for K being commutative Ring
for pK being FinSequence of K
for a being Element of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))