theorem :: MATRIX11:35

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